Theorem 2rexbidva 3038

Description: Formula-building rule for restricted existential quantifiers (deduction rule). (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 678	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒))
3	2	rexbidva 3031	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
4	3	rexbidva 3031	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∈ wcel 1977  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-rex 2902

This theorem is referenced by:  wrdl3s3  13553  bezoutlem2  15095  bezoutlem4  15097  vdwmc2  15521  lsmcom2  17893  lsmass  17906  lsmcomx  18082  lsmspsn  18905  hausdiag  21258  imasf1oxms  22104  istrkg2ld  25159  iscgra  25501  axeuclid  25643  el2wlksot  26407  el2pthsot  26408  usg2spot2nb  26592  shscom  27562  3dim0  33761  islpln5  33839  islvol5  33883  isline2  34078  isline3  34080  paddcom  34117  cdlemg2cex  34897  2reu4a  39838  wwlksnwwlksnon  41121  wspthsnwspthsnon  41122  elwwlks2  41170  elwspths2spth  41171  fusgr2wsp2nb  41498  pgrpgt2nabl  41941  elbigolo1  42149