Theorem 2ralbii 3010

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

Syntax hints:   ↔ wb 196  ∀wral 2941

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

This theorem depends on definitions:  df-bi 197  df-ral 2946

This theorem is referenced by:  cnvso  5712  fununi  6002  dff14a  6567  isocnv2  6621  sorpss  6984  tpossym  7429  dford2  8555  isffth2  16623  ispos2  16995  issubm  17394  cntzrec  17812  oppgsubm  17838  opprirred  18748  opprsubrg  18849  gsummatr01lem3  20511  gsummatr01  20513  isbasis2g  20800  ist0-3  21197  isfbas2  21686  isclmp  22943  dfadj2  28872  adjval2  28878  cnlnadjeui  29064  adjbdln  29070  rmo4f  29464  isarchi  29864  iccllysconn  31358  dfso3  31727  elpotr  31810  dfon2  31821  f1opr  33649  3ralbii  34155  idinxpss  34224  inxpssidinxp  34227  idinxpssinxp  34228  isltrn2N  35724  fphpd  37697  isdomn3  38099  fiinfi  38195  ntrk1k3eqk13  38665  ordelordALT  39064  2reu4a  41510  issubmgm  42114