Theorem 2rexbidva 3228

Description: Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 15-Dec-2004.)

Hypothesis

Ref	Expression
2rexbidva.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
2rexbidva	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

Distinct variable groups:   𝑥,𝑦,𝜑   𝑦,𝐴

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem 2rexbidva

Step	Hyp	Ref	Expression
1		2rexbidva.1	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒))
2	1	anassrs 468	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒))
3	2	rexbidva 3225	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
4	3	rexbidva 3225	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  ∃wrex 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  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-rex 3070

This theorem is referenced by:  2reu4lem  4456  wrdl3s3  14677  bezoutlem2  16248  bezoutlem4  16250  vdwmc2  16680  lsmcom2  19260  lsmass  19275  lsmcomx  19457  lsmspsn  20346  hausdiag  22796  imasf1oxms  23645  istrkg2ld  26821  iscgra  27170  axeuclid  27331  elwwlks2  28331  elwspths2spth  28332  fusgr2wsp2nb  28698  shscom  29681  lsmssass  31590  sategoelfvb  33381  3dim0  37471  islpln5  37549  islvol5  37593  isline2  37788  isline3  37790  paddcom  37827  cdlemg2cex  38605  prprspr2  44970  pgrpgt2nabl  45702  elbigolo1  45903