Theorem 2ralbii 3079

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

Syntax hints:   ↔ wb 209  ∀wral 3051

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

This theorem depends on definitions:  df-bi 210  df-ral 3056

This theorem is referenced by:  ralnex3  3172  rmo4f  3637  2reu4lem  4423  cnvso  6131  fununi  6433  dff14a  7060  isocnv2  7118  f1opr  7245  sorpss  7494  tpossym  7978  dford2  9213  isffth2  17377  ispos2  17776  issubm  18184  cntzrec  18682  oppgsubm  18708  opprirred  19674  opprsubrg  19775  gsummatr01lem3  21508  gsummatr01  21510  isbasis2g  21799  ist0-3  22196  isfbas2  22686  isclmp  23948  dfadj2  29920  adjval2  29926  cnlnadjeui  30112  adjbdln  30118  isarchi  31109  prmidl0  31294  dff15  32723  iccllysconn  32879  dfso3  33333  elpotr  33427  dfon2  33438  xpord3ind  33480  3ralbii  36074  idinxpss  36134  inxpssidinxp  36137  idinxpssinxp  36138  dfeldisj5  36518  isltrn2N  37820  isdomn5  39834  fphpd  40282  isdomn3  40673  fiinfi  40797  ntrk1k3eqk13  41278  ordelordALT  41771  disjinfi  42345  issubmgm  44959  isthinc2  45919  isthinc3  45920