Theorem 2rexbidva 3225

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∈ wcel 2142  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-rex 3087

This theorem is referenced by:  2reu4lem  4477  wrdl3s3  14975  bezoutlem2  16574  bezoutlem4  16576  vdwmc2  17015  lsmcom2  19695  lsmass  19709  lsmcomx  19896  lsmspsn  21151  hausdiag  23705  imasf1oxms  24549  mulsval  28202  mulscom  28232  addsdi  28248  mulsasslem3  28258  mulsunif2lem  28262  z12sge0  28576  istrkg2ld  28629  iscgra  29003  axeuclid  29164  elwwlks2  30169  elwspths2spth  30170  fusgr2wsp2nb  30536  shscom  31522  lsmssass  33588  sategoelfvb  35769  3dim0  40081  islpln5  40159  islvol5  40203  isline2  40398  isline3  40400  paddcom  40437  cdlemg2cex  41215  prprspr2  48124  pgrpgt2nabl  48988  elbigolo1  49179