Theorem 2ralbii 3113

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

Syntax hints:   ↔ wb 206  ∀wral 3052

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 3053

This theorem is referenced by:  3ralbii  3115  ralnex3  3119  rmo4f  3682  2reu4lem  4464  cnvso  6247  fununi  6568  dff14a  7219  isocnv2  7280  f1opr  7417  sorpss  7676  xpord3inddlem  8098  tpossym  8202  dford2  9535  isffth2  17879  ispos2  18275  issubmgm  18664  issubm  18765  cntzrec  19305  oppgsubm  19331  opprirred  20396  opprsubrng  20530  rhmimasubrng  20537  cntzsubrng  20538  opprsubrg  20564  isdomn5  20681  isdomn3  20686  gsummatr01lem3  22635  gsummatr01  22637  isbasis2g  22926  ist0-3  23323  isfbas2  23813  isclmp  25077  addsproplem4  27981  addsproplem6  27983  addsprop  27985  negsproplem4  28040  negsproplem6  28042  negsprop  28044  mulsprop  28139  dfadj2  31974  adjval2  31980  cnlnadjeui  32166  adjbdln  32172  isarchi  33261  prmidl0  33528  ply1dg3rt0irred  33662  dff15  35246  iccllysconn  35451  dfso3  35921  elpotr  35980  dfon2  35991  idinxpss  38656  inxpssidinxp  38660  idinxpssinxp  38661  dfdisjALTV5a  39141  dfeldisj5  39151  dfeldisj5a  39152  isltrn2N  40583  hashnexinj  42584  fphpd  43265  fiinfi  44021  ntrk1k3eqk13  44498  ordelordALT  44985  dfac5prim  45438  disjinfi  45643  isthinc2  49910  isthinc3  49911