Theorem rcla42ev 1928

Description: 2-variable restricted existential specialization, using 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 groups:   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 1924	. . . 4 ⊢ ((B ∈ D ⋀ ψ) → ∃y ∈ D χ)
3	2	anim2i 342	. . 3 ⊢ ((A ∈ C ⋀ (B ∈ D ⋀ ψ)) → (A ∈ C ⋀ ∃y ∈ D χ))
4	3	3impb 841	. 2 ⊢ ((A ∈ C ⋀ B ∈ D ⋀ ψ) → (A ∈ C ⋀ ∃y ∈ D χ))
5		rcla42v.1	. . . 4 ⊢ (x = A → (φ ↔ χ))
6	5	rexbidv 1711	. . 3 ⊢ (x = A → (∃y ∈ D φ ↔ ∃y ∈ D χ))
7	6	rcla4ev 1924	. 2 ⊢ ((A ∈ C ⋀ ∃y ∈ D χ) → ∃x ∈ C ∃y ∈ D φ)
8	4, 7	syl 10	1 ⊢ ((A ∈ C ⋀ B ∈ D ⋀ ψ) → ∃x ∈ C ∃y ∈ D φ)

Syntax hints:   → wi 3   ↔ wb 153   ⋀ wa 230   ⋀ w3a 787   = wceq 997   ∈ wcel 999  ∃wrex 1693

This theorem is referenced by:  rcla4eopr 4048  2dom 4488  unxpdomlem 4908  retopbas 7740  blelrn 7933  methausi 7966  blssioo 7998  dtt2 10697

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-3an 789  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518  df-rex 1697  df-v 1859

Copyright terms: Public domain