Theorem 2rexbidva 3201

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

Hypothesis

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

Assertion

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

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

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

Proof of Theorem 2rexbidva

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  ∃wrex 3054

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3055

This theorem is referenced by:  2reu4lem  4488  wrdl3s3  14935  bezoutlem2  16517  bezoutlem4  16519  vdwmc2  16957  lsmcom2  19592  lsmass  19606  lsmcomx  19793  lsmspsn  20998  hausdiag  23539  imasf1oxms  24384  mulsval  28019  mulscom  28049  addsdi  28065  mulsasslem3  28075  mulsunif2lem  28079  zs12ge0  28349  istrkg2ld  28394  iscgra  28743  axeuclid  28897  elwwlks2  29903  elwspths2spth  29904  fusgr2wsp2nb  30270  shscom  31255  lsmssass  33380  sategoelfvb  35413  3dim0  39458  islpln5  39536  islvol5  39580  isline2  39775  isline3  39777  paddcom  39814  cdlemg2cex  40592  prprspr2  47523  pgrpgt2nabl  48358  elbigolo1  48550