Theorem 2ralbii 3104

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

Syntax hints:   ↔ wb 206  ∀wral 3044

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

This theorem depends on definitions:  df-bi 207  df-ral 3045

This theorem is referenced by:  3ralbii  3106  ralnex3  3110  rmo4f  3695  2reu4lem  4473  cnvso  6236  fununi  6557  dff14a  7207  isocnv2  7268  f1opr  7405  sorpss  7664  xpord3inddlem  8087  tpossym  8191  dford2  9516  isffth2  17825  ispos2  18221  issubmgm  18576  issubm  18677  cntzrec  19215  oppgsubm  19241  opprirred  20307  opprsubrng  20444  rhmimasubrng  20451  cntzsubrng  20452  opprsubrg  20478  isdomn5  20595  isdomn3  20600  gsummatr01lem3  22542  gsummatr01  22544  isbasis2g  22833  ist0-3  23230  isfbas2  23720  isclmp  24995  addsproplem4  27884  addsproplem6  27886  addsprop  27888  negsproplem4  27942  negsproplem6  27944  negsprop  27946  mulsprop  28038  dfadj2  31829  adjval2  31835  cnlnadjeui  32021  adjbdln  32027  isarchi  33124  prmidl0  33387  ply1dg3rt0irred  33518  dff15  35051  iccllysconn  35223  dfso3  35693  elpotr  35755  dfon2  35766  idinxpss  38286  inxpssidinxp  38290  idinxpssinxp  38291  dfeldisj5  38699  isltrn2N  40099  hashnexinj  42101  fphpd  42789  fiinfi  43546  ntrk1k3eqk13  44023  ordelordALT  44511  dfac5prim  44964  disjinfi  45170  isthinc2  49405  isthinc3  49406