Theorem 2ralbii 3094

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

Syntax hints:   ↔ wb 205  ∀wral 3065

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 3070

This theorem is referenced by:  ralnex3  3191  rmo4f  3671  2reu4lem  4457  cnvso  6195  fununi  6516  dff14a  7152  isocnv2  7211  f1opr  7340  sorpss  7590  tpossym  8083  dford2  9387  isffth2  17641  ispos2  18042  issubm  18451  cntzrec  18949  oppgsubm  18978  opprirred  19953  opprsubrg  20054  gsummatr01lem3  21815  gsummatr01  21817  isbasis2g  22107  ist0-3  22505  isfbas2  22995  isclmp  24269  dfadj2  30256  adjval2  30262  cnlnadjeui  30448  adjbdln  30454  isarchi  31445  prmidl0  31635  dff15  33065  iccllysconn  33221  dfso3  33673  elpotr  33766  dfon2  33777  xpord3ind  33809  3ralbii  36396  idinxpss  36455  inxpssidinxp  36458  idinxpssinxp  36459  dfeldisj5  36839  isltrn2N  38141  isdomn5  40178  fphpd  40645  isdomn3  41036  fiinfi  41187  ntrk1k3eqk13  41667  ordelordALT  42164  disjinfi  42738  issubmgm  45354  isthinc2  46314  isthinc3  46315