Theorem 2ralbii 3108

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

Syntax hints:   ↔ wb 206  ∀wral 3044

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

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

This theorem is referenced by:  3ralbii  3110  ralnex3  3114  rmo4f  3706  2reu4lem  4485  cnvso  6261  fununi  6591  dff14a  7245  isocnv2  7306  f1opr  7445  sorpss  7704  xpord3inddlem  8133  tpossym  8237  dford2  9573  isffth2  17880  ispos2  18276  issubmgm  18629  issubm  18730  cntzrec  19268  oppgsubm  19294  opprirred  20331  opprsubrng  20468  rhmimasubrng  20475  cntzsubrng  20476  opprsubrg  20502  isdomn5  20619  isdomn3  20624  gsummatr01lem3  22544  gsummatr01  22546  isbasis2g  22835  ist0-3  23232  isfbas2  23722  isclmp  24997  addsproplem4  27879  addsproplem6  27881  addsprop  27883  negsproplem4  27937  negsproplem6  27939  negsprop  27941  mulsprop  28033  dfadj2  31814  adjval2  31820  cnlnadjeui  32006  adjbdln  32012  isarchi  33136  prmidl0  33421  ply1dg3rt0irred  33551  dff15  35074  iccllysconn  35237  dfso3  35707  elpotr  35769  dfon2  35780  idinxpss  38300  inxpssidinxp  38304  idinxpssinxp  38305  dfeldisj5  38713  isltrn2N  40114  hashnexinj  42116  fphpd  42804  fiinfi  43562  ntrk1k3eqk13  44039  ordelordALT  44527  dfac5prim  44980  disjinfi  45186  isthinc2  49409  isthinc3  49410