Theorem 2ralbii 3140

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

Syntax hints:   ↔ wb 209  ∀wral 3079

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

This theorem depends on definitions:  df-bi 210  df-ral 3080

This theorem is referenced by:  3ralbii  3142  ralnex3  3146  rmo4f  3698  2reu4lem  4484  cnvso  6289  fununi  6611  dff14a  7268  isocnv2  7329  f1opr  7466  sorpss  7725  xpord3inddlem  8146  tpossym  8250  dford2  9585  isffth2  17970  ispos2  18366  issubmgm  18755  issubm  18856  cntzrec  19401  oppgsubm  19427  opprirred  20500  opprsubrng  20658  rhmimasubrng  20665  cntzsubrng  20666  opprsubrg  20692  isdomn5  20809  isdomn3  20813  prmidl0  21478  gsummatr01lem3  22814  gsummatr01  22816  isbasis2g  23105  ist0-3  23502  isfbas2  23992  isclmp  25256  addsproplem4  28165  addsproplem6  28167  addsprop  28169  negsproplem4  28224  negsproplem6  28226  negsprop  28228  mulsprop  28323  dfadj2  32237  adjval2  32243  cnlnadjeui  32429  adjbdln  32435  isarchi  33502  ply1dg3rt0irred  33874  dff15  35472  iccllysconn  35742  dfso3  36212  elpotr  36271  dfon2  36282  idinxpss  38967  inxpssidinxp  38971  idinxpssinxp  38972  dfdisjALTV5a  39452  dfeldisj5  39462  dfeldisj5a  39463  isltrn2N  40894  hashnexinj  42895  fphpd  43543  fiinfi  44299  ntrk1k3eqk13  44776  ordelordALT  45246  dfac5prim  45699  disjinfi  45910  isthinc2  50198  isthinc3  50199