Theorem 2ralbii 3135

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

Syntax hints:   ↔ wb 207  ∀wral 3107

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

This theorem depends on definitions:  df-bi 208  df-ral 3112

This theorem is referenced by:  ralnex3  3228  rmo4f  3665  2reu4lem  4385  cnvso  6021  fununi  6306  dff14a  6900  isocnv2  6954  f1opr  7076  sorpss  7319  tpossym  7782  dford2  8936  isffth2  17019  ispos2  17391  issubm  17790  cntzrec  18209  oppgsubm  18235  opprirred  19146  opprsubrg  19250  gsummatr01lem3  20954  gsummatr01  20956  isbasis2g  21244  ist0-3  21641  isfbas2  22131  isclmp  23388  dfadj2  29349  adjval2  29355  cnlnadjeui  29541  adjbdln  29547  isarchi  30445  dff15  31963  iccllysconn  32107  dfso3  32560  elpotr  32636  dfon2  32647  3ralbii  35063  idinxpss  35123  inxpssidinxp  35126  idinxpssinxp  35127  dfeldisj5  35506  isltrn2N  36808  fphpd  38919  isdomn3  39310  fiinfi  39438  ntrk1k3eqk13  39906  ordelordALT  40431  issubmgm  43560