Theorem 2ralbii 3125

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

Syntax hints:   ↔ wb 206  ∀wral 3058

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

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

This theorem is referenced by:  3ralbii  3127  ralnex3  3131  rmo4f  3743  2reu4lem  4527  cnvso  6309  fununi  6642  dff14a  7289  isocnv2  7350  f1opr  7488  sorpss  7746  xpord3inddlem  8177  tpossym  8281  dford2  9657  isffth2  17969  ispos2  18372  issubmgm  18727  issubm  18828  cntzrec  19366  oppgsubm  19395  opprirred  20438  opprsubrng  20575  rhmimasubrng  20582  cntzsubrng  20583  opprsubrg  20609  isdomn5  20726  isdomn3  20731  gsummatr01lem3  22678  gsummatr01  22680  isbasis2g  22970  ist0-3  23368  isfbas2  23858  isclmp  25143  addsproplem4  28019  addsproplem6  28021  addsprop  28023  negsproplem4  28077  negsproplem6  28079  negsprop  28081  mulsprop  28170  dfadj2  31913  adjval2  31919  cnlnadjeui  32105  adjbdln  32111  isarchi  33171  prmidl0  33457  ply1dg3rt0irred  33586  dff15  35076  iccllysconn  35234  dfso3  35699  elpotr  35762  dfon2  35773  idinxpss  38293  inxpssidinxp  38297  idinxpssinxp  38298  dfeldisj5  38702  isltrn2N  40102  hashnexinj  42109  fphpd  42803  fiinfi  43562  ntrk1k3eqk13  44039  ordelordALT  44534  disjinfi  45134  isthinc2  48821  isthinc3  48822