Theorem rcla42ev 1405

Description: 2-variable restricted existential specialization with implicit substitution.

Hypotheses

Ref	Expression
rcla42v.1	⊢ (x = A → (φ ↔ χ))
rcla42v.2	⊢ (y = B → (χ ↔ ψ))

Assertion

Ref	Expression
rcla42ev	⊢ (((A ∈ C ∧ B ∈ D) ∧ ψ) → ∃x ∈ C ∃y ∈ D φ)

Distinct variable group(s):   x,y,A   x,C   x,D   y,B   y,D   χ,x   ψ,y

Proof of Theorem rcla42ev

Step	Hyp	Ref	Expression
1		rcla42v.2	. . . . 5 ⊢ (y = B → (χ ↔ ψ))
2	1	rcla4ev 1403	. . . 4 ⊢ ((B ∈ D ∧ ψ) → ∃y ∈ D χ)
3	2	anim2i 270	. . 3 ⊢ ((A ∈ C ∧ (B ∈ D ∧ ψ)) → (A ∈ C ∧ ∃y ∈ D χ))
4	3	anassrs 338	. 2 ⊢ (((A ∈ C ∧ B ∈ D) ∧ ψ) → (A ∈ C ∧ ∃y ∈ D χ))
5		rcla42v.1	. . . 4 ⊢ (x = A → (φ ↔ χ))
6	5	birexdv 1220	. . 3 ⊢ (x = A → (∃y ∈ D φ ↔ ∃y ∈ D χ))
7	6	rcla4ev 1403	. 2 ⊢ ((A ∈ C ∧ ∃y ∈ D χ) → ∃x ∈ C ∃y ∈ D φ)
8	4, 7	syl 12	1 ⊢ (((A ∈ C ∧ B ∈ D) ∧ ψ) → ∃x ∈ C ∃y ∈ D φ)

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196   = wceq 1091   ∈ wcel 1092  ∃wrex 1202

This theorem is referenced by:  2dom 3332  unxpdomlem 3649  znq 4630  qaddclt 4642  qnegclt 4643  qmulclt 4644  qrecclt 4646  pjthlem14 5238  pjpjtht 5262  shscl 5282  shsvat 5285  shunss 5338  spanunsn 5482  pjjs 5585

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-rex 1206  df-v 1349

metamath.org