Theorem 2ralbii 3134

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

Syntax hints:   ↔ wb 206  ∀wral 3067

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

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

This theorem is referenced by:  3ralbii  3136  ralnex3  3140  rmo4f  3757  2reu4lem  4545  cnvso  6319  fununi  6653  dff14a  7307  isocnv2  7367  f1opr  7506  sorpss  7763  xpord3inddlem  8195  tpossym  8299  dford2  9689  isffth2  17983  ispos2  18385  issubmgm  18740  issubm  18838  cntzrec  19376  oppgsubm  19405  opprirred  20448  opprsubrng  20585  rhmimasubrng  20592  cntzsubrng  20593  opprsubrg  20621  isdomn5  20732  isdomn3  20737  gsummatr01lem3  22684  gsummatr01  22686  isbasis2g  22976  ist0-3  23374  isfbas2  23864  isclmp  25149  addsproplem4  28023  addsproplem6  28025  addsprop  28027  negsproplem4  28081  negsproplem6  28083  negsprop  28085  mulsprop  28174  dfadj2  31917  adjval2  31923  cnlnadjeui  32109  adjbdln  32115  isarchi  33162  prmidl0  33443  ply1dg3rt0irred  33572  dff15  35060  iccllysconn  35218  dfso3  35682  elpotr  35745  dfon2  35756  idinxpss  38268  inxpssidinxp  38272  idinxpssinxp  38273  dfeldisj5  38677  isltrn2N  40077  hashnexinj  42085  fphpd  42772  fiinfi  43535  ntrk1k3eqk13  44012  ordelordALT  44508  disjinfi  45099  isthinc2  48689  isthinc3  48690