Theorem 2ralbii 3137

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

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

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

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

This theorem is used by:  3ralbii  3139  ralnex3  3143  rmo4f  3692  2reu4lem  4478  cnvso  6294  fununi  6620  dff14a  7278  dff15  7280  isocnv2  7343  f1opr  7480  sorpss  7748  xpord3inddlem  8177  tpossym  8282  dford2  9628  isffth2  18102  ispos2  18498  issubmgm  18900  issubm  19007  cntzrec  19559  oppgsubm  19585  dfring3  20527  opprirred  20661  opprsubrng  20820  rhmimasubrng  20827  cntzsubrng  20828  opprsubrg  20854  isdomn5  20971  isdomn3  20975  prmidl0  21643  gsummatr01lem3  22981  gsummatr01  22983  isbasis2g  23275  ist0-3  23672  isfbas2  24163  isclmp  25427  addsproplem4  28367  addsproplem6  28369  addsprop  28371  negsproplem4  28426  negsproplem6  28428  negsprop  28430  mulsprop  28525  dfadj2  32496  adjval2  32502  cnlnadjeui  32688  adjbdln  32694  isarchi  33793  ply1dg3rt0irred  34166  iccllysconn  36105  dfso3  36581  elpotr  36639  dfon2  36650  idinxpss  39359  inxpssidinxp  39363  idinxpssinxp  39364  dfdisjALTV5a  39844  dfeldisj5  39854  dfeldisj5a  39855  isltrn2N  41286  hashnexinj  43287  fphpd  43932  fiinfi  44683  ntrk1k3eqk13  45159  ordelordALT  45628  dfac5prim  46088  disjinfi  46315  isthinc2  50663  isthinc3  50664