Theorem 2ralbii 3113

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

Syntax hints:   ↔ wb 206  ∀wral 3052

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

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

This theorem is referenced by:  3ralbii  3115  ralnex3  3119  rmo4f  3695  2reu4lem  4478  cnvso  6254  fununi  6575  dff14a  7226  isocnv2  7287  f1opr  7424  sorpss  7683  xpord3inddlem  8106  tpossym  8210  dford2  9541  isffth2  17854  ispos2  18250  issubmgm  18639  issubm  18740  cntzrec  19277  oppgsubm  19303  opprirred  20370  opprsubrng  20504  rhmimasubrng  20511  cntzsubrng  20512  opprsubrg  20538  isdomn5  20655  isdomn3  20660  gsummatr01lem3  22613  gsummatr01  22615  isbasis2g  22904  ist0-3  23301  isfbas2  23791  isclmp  25065  addsproplem4  27980  addsproplem6  27982  addsprop  27984  negsproplem4  28039  negsproplem6  28041  negsprop  28043  mulsprop  28138  dfadj2  31973  adjval2  31979  cnlnadjeui  32165  adjbdln  32171  isarchi  33276  prmidl0  33543  ply1dg3rt0irred  33677  dff15  35261  iccllysconn  35466  dfso3  35936  elpotr  35995  dfon2  36006  idinxpss  38569  inxpssidinxp  38573  idinxpssinxp  38574  dfdisjALTV5a  39054  dfeldisj5  39064  dfeldisj5a  39065  isltrn2N  40496  hashnexinj  42498  fphpd  43173  fiinfi  43929  ntrk1k3eqk13  44406  ordelordALT  44893  dfac5prim  45346  disjinfi  45551  isthinc2  49779  isthinc3  49780