Theorem 2ralbii 3146

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

Hypothesis

Ref	Expression
2ralbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

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

Proof of Theorem 2ralbii

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

Syntax hints:   ↔ wb 209  ∀wral 3085

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

This theorem depends on definitions:  df-bi 210  df-ral 3086

This theorem is referenced by:  3ralbii  3148  ralnex3  3152  rmo4f  3707  2reu4lem  4489  cnvso  6290  fununi  6612  dff14a  7269  isocnv2  7330  f1opr  7467  sorpss  7726  xpord3inddlem  8149  tpossym  8253  dford2  9588  isffth2  17974  ispos2  18370  issubmgm  18759  issubm  18860  cntzrec  19405  oppgsubm  19431  opprirred  20503  opprsubrng  20643  rhmimasubrng  20650  cntzsubrng  20651  opprsubrg  20677  isdomn5  20794  isdomn3  20798  prmidl0  21446  gsummatr01lem3  22782  gsummatr01  22784  isbasis2g  23073  ist0-3  23470  isfbas2  23960  isclmp  25224  addsproplem4  28130  addsproplem6  28132  addsprop  28134  negsproplem4  28189  negsproplem6  28191  negsprop  28193  mulsprop  28288  dfadj2  32177  adjval2  32183  cnlnadjeui  32369  adjbdln  32375  isarchi  33442  ply1dg3rt0irred  33818  dff15  35415  iccllysconn  35640  dfso3  36110  elpotr  36169  dfon2  36180  idinxpss  38856  inxpssidinxp  38860  idinxpssinxp  38861  dfdisjALTV5a  39341  dfeldisj5  39351  dfeldisj5a  39352  isltrn2N  40783  hashnexinj  42784  fphpd  43434  fiinfi  44190  ntrk1k3eqk13  44667  ordelordALT  45137  dfac5prim  45590  disjinfi  45801  isthinc2  50082  isthinc3  50083