Theorem 2ralbii 3128

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

Syntax hints:   ↔ wb 205  ∀wral 3061

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

This theorem is referenced by:  3ralbii  3130  ralnex3  3134  rmo4f  3731  2reu4lem  4525  cnvso  6287  fununi  6623  dff14a  7268  isocnv2  7327  f1opr  7464  sorpss  7717  xpord3inddlem  8139  tpossym  8242  dford2  9614  isffth2  17866  ispos2  18267  issubm  18683  cntzrec  19199  oppgsubm  19228  opprirred  20235  opprsubrg  20339  isdomn5  20916  gsummatr01lem3  22158  gsummatr01  22160  isbasis2g  22450  ist0-3  22848  isfbas2  23338  isclmp  24612  addsproplem4  27453  addsproplem6  27455  addsprop  27457  negsproplem4  27502  negsproplem6  27504  negsprop  27506  mulsprop  27583  dfadj2  31133  adjval2  31139  cnlnadjeui  31325  adjbdln  31331  isarchi  32323  prmidl0  32564  dff15  34082  iccllysconn  34236  dfso3  34684  elpotr  34748  dfon2  34759  idinxpss  37176  inxpssidinxp  37180  idinxpssinxp  37181  dfeldisj5  37586  isltrn2N  38986  fphpd  41544  isdomn3  41936  fiinfi  42314  ntrk1k3eqk13  42791  ordelordALT  43288  disjinfi  43881  issubmgm  46549  opprsubrng  46728  rhmimasubrng  46735  cntzsubrng  46736  isthinc2  47632  isthinc3  47633