Theorem 2ralbii 3114

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

Syntax hints:   ↔ wb 207  ∀wral 3053

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

This theorem depends on definitions:  df-bi 208  df-ral 3054

This theorem is referenced by:  3ralbii  3116  ralnex3  3120  rmo4f  3676  2reu4lem  4451  cnvso  6239  fununi  6560  dff14a  7214  isocnv2  7275  f1opr  7412  sorpss  7671  xpord3inddlem  8094  tpossym  8198  dford2  9532  isffth2  17876  ispos2  18272  issubmgm  18661  issubm  18762  cntzrec  19302  oppgsubm  19328  opprirred  20393  opprsubrng  20531  rhmimasubrng  20538  cntzsubrng  20539  opprsubrg  20565  isdomn5  20682  isdomn3  20687  gsummatr01lem3  22640  gsummatr01  22642  isbasis2g  22931  ist0-3  23328  isfbas2  23818  isclmp  25082  addsproplem4  27982  addsproplem6  27984  addsprop  27986  negsproplem4  28041  negsproplem6  28043  negsprop  28045  mulsprop  28140  dfadj2  31974  adjval2  31980  cnlnadjeui  32166  adjbdln  32172  isarchi  33263  prmidl0  33533  ply1dg3rt0irred  33667  dff15  35265  iccllysconn  35478  dfso3  35948  elpotr  36007  dfon2  36018  idinxpss  38685  inxpssidinxp  38689  idinxpssinxp  38690  dfdisjALTV5a  39170  dfeldisj5  39180  dfeldisj5a  39181  isltrn2N  40612  hashnexinj  42613  fphpd  43261  fiinfi  44017  ntrk1k3eqk13  44494  ordelordALT  44981  dfac5prim  45434  disjinfi  45639  isthinc2  49910  isthinc3  49911