Theorem 2ralbii 2981

Description: Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)

Hypothesis

Ref	Expression
ralbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
2ralbii	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Proof of Theorem 2ralbii

Step	Hyp	Ref	Expression
1		ralbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	ralbii 2980	. 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)
3	2	ralbii 2980	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   ↔ wb 196  ∀wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-ral 2917

This theorem is referenced by:  cnvso  5674  fununi  5964  dff14a  6527  isocnv2  6581  sorpss  6942  tpossym  7384  dford2  8517  isffth2  16576  ispos2  16948  issubm  17347  cntzrec  17766  oppgsubm  17792  opprirred  18702  opprsubrg  18801  gsummatr01lem3  20463  gsummatr01  20465  isbasis2g  20752  ist0-3  21149  isfbas2  21639  isclmp  22897  dfadj2  28744  adjval2  28750  cnlnadjeui  28936  adjbdln  28942  rmo4f  29337  isarchi  29736  iccllysconn  31232  dfso3  31601  elpotr  31686  dfon2  31697  f1opr  33519  3ralbii  34013  idinxpss  34083  inxpssidinxp  34086  idinxpssinxp  34087  isltrn2N  35406  fphpd  37380  isdomn3  37782  fiinfi  37878  ntrk1k3eqk13  38348  ordelordALT  38747  2reu4a  41189  issubmgm  41789