Theorem 2rexbidva 3264

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 3261	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
4	3	rexbidva 3261	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∈ wcel 2083  ∃wrex 3108

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-rex 3113

This theorem is referenced by:  2reu4lem  4385  wrdl3s3  14164  bezoutlem2  15721  bezoutlem4  15723  vdwmc2  16148  lsmcom2  18514  lsmass  18527  lsmcomx  18703  lsmspsn  19550  hausdiag  21941  imasf1oxms  22786  istrkg2ld  25932  iscgra  26281  axeuclid  26436  elwwlks2  27431  elwspths2spth  27432  fusgr2wsp2nb  27801  shscom  28783  sategoelfvb  32276  3dim0  36145  islpln5  36223  islvol5  36267  isline2  36462  isline3  36464  paddcom  36501  cdlemg2cex  37279  prprspr2  43184  pgrpgt2nabl  43916  elbigolo1  44120