Theorem 2ralbii 3112

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

Syntax hints:   ↔ wb 206  ∀wral 3051

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

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

This theorem is referenced by:  3ralbii  3114  ralnex3  3118  rmo4f  3681  2reu4lem  4463  cnvso  6252  fununi  6573  dff14a  7225  isocnv2  7286  f1opr  7423  sorpss  7682  xpord3inddlem  8104  tpossym  8208  dford2  9541  isffth2  17885  ispos2  18281  issubmgm  18670  issubm  18771  cntzrec  19311  oppgsubm  19337  opprirred  20402  opprsubrng  20536  rhmimasubrng  20543  cntzsubrng  20544  opprsubrg  20570  isdomn5  20687  isdomn3  20692  gsummatr01lem3  22622  gsummatr01  22624  isbasis2g  22913  ist0-3  23310  isfbas2  23800  isclmp  25064  addsproplem4  27964  addsproplem6  27966  addsprop  27968  negsproplem4  28023  negsproplem6  28025  negsprop  28027  mulsprop  28122  dfadj2  31956  adjval2  31962  cnlnadjeui  32148  adjbdln  32154  isarchi  33243  prmidl0  33510  ply1dg3rt0irred  33644  dff15  35227  iccllysconn  35432  dfso3  35902  elpotr  35961  dfon2  35972  idinxpss  38639  inxpssidinxp  38643  idinxpssinxp  38644  dfdisjALTV5a  39124  dfeldisj5  39134  dfeldisj5a  39135  isltrn2N  40566  hashnexinj  42567  fphpd  43244  fiinfi  44000  ntrk1k3eqk13  44477  ordelordALT  44964  dfac5prim  45417  disjinfi  45622  isthinc2  49895  isthinc3  49896