Theorem 2ralbii 3139

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

This proof depends on syntax axioms:   ↔ wb 209  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838

This proof depends on definitions:  df-bi 210  df-ral 3079

This theorem is used by:  3ralbii  3141  ralnex3  3145  rmo4f  3697  2reu4lem  4483  cnvso  6289  fununi  6611  dff14a  7268  isocnv2  7329  f1opr  7468  sorpss  7727  xpord3inddlem  8148  tpossym  8252  dford2  9587  isffth2  17981  ispos2  18377  issubmgm  18766  issubm  18867  cntzrec  19412  oppgsubm  19438  opprirred  20511  opprsubrng  20669  rhmimasubrng  20676  cntzsubrng  20677  opprsubrg  20703  isdomn5  20820  isdomn3  20824  prmidl0  21489  gsummatr01lem3  22825  gsummatr01  22827  isbasis2g  23116  ist0-3  23513  isfbas2  24003  isclmp  25267  addsproplem4  28176  addsproplem6  28178  addsprop  28180  negsproplem4  28235  negsproplem6  28237  negsprop  28239  mulsprop  28334  dfadj2  32248  adjval2  32254  cnlnadjeui  32440  adjbdln  32446  isarchi  33511  ply1dg3rt0irred  33883  dff15  35481  iccllysconn  35750  dfso3  36220  elpotr  36279  dfon2  36290  idinxpss  38995  inxpssidinxp  38999  idinxpssinxp  39000  dfdisjALTV5a  39480  dfeldisj5  39490  dfeldisj5a  39491  isltrn2N  40922  hashnexinj  42923  fphpd  43571  fiinfi  44327  ntrk1k3eqk13  44804  ordelordALT  45274  dfac5prim  45727  disjinfi  45938  isthinc2  50226  isthinc3  50227