Theorem 2ralbii 3129

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

Syntax hints:   ↔ wb 205  ∀wral 3062

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

This theorem depends on definitions:  df-bi 206  df-ral 3063

This theorem is referenced by:  3ralbii  3131  ralnex3  3135  rmo4f  3732  2reu4lem  4526  cnvso  6288  fununi  6624  dff14a  7269  isocnv2  7328  f1opr  7465  sorpss  7718  xpord3inddlem  8140  tpossym  8243  dford2  9615  isffth2  17867  ispos2  18268  issubm  18684  cntzrec  19200  oppgsubm  19229  opprirred  20236  opprsubrg  20340  isdomn5  20917  gsummatr01lem3  22159  gsummatr01  22161  isbasis2g  22451  ist0-3  22849  isfbas2  23339  isclmp  24613  addsproplem4  27456  addsproplem6  27458  addsprop  27460  negsproplem4  27505  negsproplem6  27507  negsprop  27509  mulsprop  27586  dfadj2  31138  adjval2  31144  cnlnadjeui  31330  adjbdln  31336  isarchi  32328  prmidl0  32569  dff15  34087  iccllysconn  34241  dfso3  34689  elpotr  34753  dfon2  34764  idinxpss  37181  inxpssidinxp  37185  idinxpssinxp  37186  dfeldisj5  37591  isltrn2N  38991  fphpd  41554  isdomn3  41946  fiinfi  42324  ntrk1k3eqk13  42801  ordelordALT  43298  disjinfi  43891  issubmgm  46559  opprsubrng  46738  rhmimasubrng  46745  cntzsubrng  46746  isthinc2  47642  isthinc3  47643