Theorem 2ralbii 3142

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 3113	. 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)
3	2	ralbii 3113	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

This proof depends on syntax axioms:   ↔ wb 209  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3082

This theorem is used by:  3ralbii  3144  ralnex3  3148  rmo4f  3700  2reu4lem  4486  cnvso  6293  fununi  6615  dff14a  7273  dff15  7275  isocnv2  7338  f1opr  7475  sorpss  7735  xpord3inddlem  8156  tpossym  8260  dford2  9596  isffth2  17997  ispos2  18393  issubmgm  18792  issubm  18898  cntzrec  19450  oppgsubm  19476  opprirred  20550  opprsubrng  20708  rhmimasubrng  20715  cntzsubrng  20716  opprsubrg  20742  isdomn5  20859  isdomn3  20863  prmidl0  21528  gsummatr01lem3  22864  gsummatr01  22866  isbasis2g  23155  ist0-3  23552  isfbas2  24043  isclmp  25307  addsproplem4  28216  addsproplem6  28218  addsprop  28220  negsproplem4  28275  negsproplem6  28277  negsprop  28279  mulsprop  28374  dfadj2  32308  adjval2  32314  cnlnadjeui  32500  adjbdln  32506  isarchi  33566  ply1dg3rt0irred  33938  iccllysconn  35779  dfso3  36249  elpotr  36308  dfon2  36319  idinxpss  39025  inxpssidinxp  39029  idinxpssinxp  39030  dfdisjALTV5a  39510  dfeldisj5  39520  dfeldisj5a  39521  isltrn2N  40952  hashnexinj  42953  fphpd  43601  fiinfi  44357  ntrk1k3eqk13  44834  ordelordALT  45304  dfac5prim  45757  disjinfi  45968  isthinc2  50255  isthinc3  50256