Theorem 2ralbii 3091

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

Syntax hints:   ↔ wb 205  ∀wral 3063

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

This theorem depends on definitions:  df-bi 206  df-ral 3068

This theorem is referenced by:  ralnex3  3189  rmo4f  3665  2reu4lem  4453  cnvso  6180  fununi  6493  dff14a  7124  isocnv2  7182  f1opr  7309  sorpss  7559  tpossym  8045  dford2  9308  isffth2  17548  ispos2  17948  issubm  18357  cntzrec  18855  oppgsubm  18884  opprirred  19859  opprsubrg  19960  gsummatr01lem3  21714  gsummatr01  21716  isbasis2g  22006  ist0-3  22404  isfbas2  22894  isclmp  24166  dfadj2  30148  adjval2  30154  cnlnadjeui  30340  adjbdln  30346  isarchi  31338  prmidl0  31528  dff15  32956  iccllysconn  33112  dfso3  33566  elpotr  33663  dfon2  33674  xpord3ind  33727  3ralbii  36315  idinxpss  36375  inxpssidinxp  36378  idinxpssinxp  36379  dfeldisj5  36759  isltrn2N  38061  isdomn5  40099  fphpd  40554  isdomn3  40945  fiinfi  41069  ntrk1k3eqk13  41549  ordelordALT  42046  disjinfi  42620  issubmgm  45231  isthinc2  46191  isthinc3  46192