Theorem 2ralbii 3107

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

Syntax hints:   ↔ wb 206  ∀wral 3047

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

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

This theorem is referenced by:  3ralbii  3109  ralnex3  3113  rmo4f  3689  2reu4lem  4469  cnvso  6235  fununi  6556  dff14a  7204  isocnv2  7265  f1opr  7402  sorpss  7661  xpord3inddlem  8084  tpossym  8188  dford2  9510  isffth2  17825  ispos2  18221  issubmgm  18610  issubm  18711  cntzrec  19248  oppgsubm  19274  opprirred  20340  opprsubrng  20474  rhmimasubrng  20481  cntzsubrng  20482  opprsubrg  20508  isdomn5  20625  isdomn3  20630  gsummatr01lem3  22572  gsummatr01  22574  isbasis2g  22863  ist0-3  23260  isfbas2  23750  isclmp  25024  addsproplem4  27915  addsproplem6  27917  addsprop  27919  negsproplem4  27973  negsproplem6  27975  negsprop  27977  mulsprop  28069  dfadj2  31865  adjval2  31871  cnlnadjeui  32057  adjbdln  32063  isarchi  33151  prmidl0  33415  ply1dg3rt0irred  33546  dff15  35096  iccllysconn  35294  dfso3  35764  elpotr  35823  dfon2  35834  idinxpss  38354  inxpssidinxp  38358  idinxpssinxp  38359  dfeldisj5  38767  isltrn2N  40167  hashnexinj  42169  fphpd  42857  fiinfi  43614  ntrk1k3eqk13  44091  ordelordALT  44578  dfac5prim  45031  disjinfi  45237  isthinc2  49460  isthinc3  49461