Theorem 2ralbii 3126

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

Syntax hints:   ↔ wb 205  ∀wral 3059

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 206  df-ral 3060

This theorem is referenced by:  3ralbii  3128  ralnex3  3132  rmo4f  3730  2reu4lem  4524  cnvso  6286  fununi  6622  dff14a  7271  isocnv2  7330  f1opr  7467  sorpss  7720  xpord3inddlem  8142  tpossym  8245  dford2  9617  isffth2  17871  ispos2  18272  issubmgm  18627  issubm  18720  cntzrec  19241  oppgsubm  19270  opprirred  20313  opprsubrng  20447  rhmimasubrng  20454  cntzsubrng  20455  opprsubrg  20483  isdomn5  21117  gsummatr01lem3  22379  gsummatr01  22381  isbasis2g  22671  ist0-3  23069  isfbas2  23559  isclmp  24844  addsproplem4  27694  addsproplem6  27696  addsprop  27698  negsproplem4  27744  negsproplem6  27746  negsprop  27748  mulsprop  27825  dfadj2  31405  adjval2  31411  cnlnadjeui  31597  adjbdln  31603  isarchi  32598  prmidl0  32843  dff15  34385  iccllysconn  34539  dfso3  34993  elpotr  35057  dfon2  35068  idinxpss  37484  inxpssidinxp  37488  idinxpssinxp  37489  dfeldisj5  37894  isltrn2N  39294  fphpd  41856  isdomn3  42248  fiinfi  42626  ntrk1k3eqk13  43103  ordelordALT  43600  disjinfi  44189  isthinc2  47729  isthinc3  47730