Theorem 2ralbii 3166

Description: Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)

Hypothesis

Ref	Expression
ralbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
2ralbii	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Proof of Theorem 2ralbii

Step	Hyp	Ref	Expression
1		ralbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	ralbii 3165	. 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)
3	2	ralbii 3165	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   ↔ wb 208  ∀wral 3138

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 209  df-ral 3143

This theorem is referenced by:  ralnex3  3262  rmo4f  3726  2reu4lem  4465  cnvso  6139  fununi  6429  dff14a  7028  isocnv2  7084  f1opr  7210  sorpss  7454  tpossym  7924  dford2  9083  isffth2  17186  ispos2  17558  issubm  17968  cntzrec  18464  oppgsubm  18490  opprirred  19452  opprsubrg  19556  gsummatr01lem3  21266  gsummatr01  21268  isbasis2g  21556  ist0-3  21953  isfbas2  22443  isclmp  23701  dfadj2  29662  adjval2  29668  cnlnadjeui  29854  adjbdln  29860  isarchi  30811  dff15  32353  iccllysconn  32497  dfso3  32950  elpotr  33026  dfon2  33037  3ralbii  35525  idinxpss  35585  inxpssidinxp  35588  idinxpssinxp  35589  dfeldisj5  35969  isltrn2N  37271  fphpd  39433  isdomn3  39824  fiinfi  39952  ntrk1k3eqk13  40420  ordelordALT  40891  issubmgm  44076