Theorem 2ralbii 3141

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

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

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

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

This theorem is used by:  3ralbii  3143  ralnex3  3147  rmo4f  3696  2reu4lem  4482  cnvso  6315  fununi  6645  dff14a  7305  dff15  7307  isocnv2  7370  f1opr  7507  sorpss  7776  xpord3inddlem  8208  tpossym  8313  dford2  9658  isffth2  18143  ispos2  18539  issubmgm  18941  issubm  19048  cntzrec  19601  oppgsubm  19627  dfring3  20569  opprirred  20703  opprsubrng  20862  rhmimasubrng  20869  cntzsubrng  20870  opprsubrg  20896  isdomn5  21013  isdomn3  21017  prmidl0  21685  gsummatr01lem3  23027  gsummatr01  23029  isbasis2g  23321  ist0-3  23718  isfbas2  24209  isclmp  25473  addsproplem4  28415  addsproplem6  28417  addsprop  28419  negsproplem4  28474  negsproplem6  28476  negsprop  28478  mulsprop  28573  dfadj2  32544  adjval2  32550  cnlnadjeui  32736  adjbdln  32742  isarchi  33842  ply1dg3rt0irred  34219  iccllysconn  36223  dfso3  36700  elpotr  36758  dfon2  36769  idinxpss  39516  inxpssidinxp  39520  idinxpssinxp  39521  dfdisjALTV5a  40001  dfeldisj5  40011  dfeldisj5a  40012  isltrn2N  41443  hashnexinj  43444  fphpd  44089  fiinfi  44835  ntrk1k3eqk13  45311  ordelordALT  45780  dfac5prim  46244  disjinfi  46480  isthinc2  50886  isthinc3  50887