Theorem 2ralbii 3168

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

Syntax hints:   ↔ wb 208  ∀wral 3140

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 3145

This theorem is referenced by:  ralnex3  3264  rmo4f  3728  2reu4lem  4467  cnvso  6141  fununi  6431  dff14a  7030  isocnv2  7086  f1opr  7212  sorpss  7456  tpossym  7926  dford2  9085  isffth2  17188  ispos2  17560  issubm  17970  cntzrec  18466  oppgsubm  18492  opprirred  19454  opprsubrg  19558  gsummatr01lem3  21268  gsummatr01  21270  isbasis2g  21558  ist0-3  21955  isfbas2  22445  isclmp  23703  dfadj2  29664  adjval2  29670  cnlnadjeui  29856  adjbdln  29862  isarchi  30813  dff15  32355  iccllysconn  32499  dfso3  32952  elpotr  33028  dfon2  33039  3ralbii  35512  idinxpss  35572  inxpssidinxp  35575  idinxpssinxp  35576  dfeldisj5  35956  isltrn2N  37258  fphpd  39420  isdomn3  39811  fiinfi  39939  ntrk1k3eqk13  40407  ordelordALT  40878  issubmgm  44063