This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem exss

Description: Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003)

Ref Expression
Assertion exss ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝑦 𝜑 ) )

Proof

Step Hyp Ref Expression
1 df-rab ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
2 1 neeq1i ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ ↔ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ≠ ∅ )
3 rabn0 ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐴 𝜑 )
4 n0 ⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } )
5 2 3 4 3bitr3i ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑧 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } )
6 vex ⊢ 𝑧 ∈ V
7 6 snss ⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ↔ { 𝑧 } ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } )
8 ssab2 ⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ⊆ 𝐴
9 sstr2 ⊢ ( { 𝑧 } ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } → ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ⊆ 𝐴 → { 𝑧 } ⊆ 𝐴 ) )
10 8 9 mpi ⊢ ( { 𝑧 } ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } → { 𝑧 } ⊆ 𝐴 )
11 7 10 sylbi ⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } → { 𝑧 } ⊆ 𝐴 )
12 simpr ⊢ ( ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) → [ 𝑧 / 𝑥 ] 𝜑 )
13 equsb1v ⊢ [ 𝑧 / 𝑥 ] 𝑥 = 𝑧
14 velsn ⊢ ( 𝑥 ∈ { 𝑧 } ↔ 𝑥 = 𝑧 )
15 14 sbbii ⊢ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ { 𝑧 } ↔ [ 𝑧 / 𝑥 ] 𝑥 = 𝑧 )
16 13 15 mpbir ⊢ [ 𝑧 / 𝑥 ] 𝑥 ∈ { 𝑧 }
17 12 16 jctil ⊢ ( ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) → ( [ 𝑧 / 𝑥 ] 𝑥 ∈ { 𝑧 } ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
18 df-clab ⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ↔ [ 𝑧 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
19 sban ⊢ ( [ 𝑧 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
20 18 19 bitri ⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
21 df-rab ⊢ { 𝑥 ∈ { 𝑧 } ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ { 𝑧 } ∧ 𝜑 ) }
22 21 eleq2i ⊢ ( 𝑧 ∈ { 𝑥 ∈ { 𝑧 } ∣ 𝜑 } ↔ 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ { 𝑧 } ∧ 𝜑 ) } )
23 df-clab ⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ { 𝑧 } ∧ 𝜑 ) } ↔ [ 𝑧 / 𝑥 ] ( 𝑥 ∈ { 𝑧 } ∧ 𝜑 ) )
24 sban ⊢ ( [ 𝑧 / 𝑥 ] ( 𝑥 ∈ { 𝑧 } ∧ 𝜑 ) ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ { 𝑧 } ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
25 22 23 24 3bitri ⊢ ( 𝑧 ∈ { 𝑥 ∈ { 𝑧 } ∣ 𝜑 } ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ { 𝑧 } ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
26 17 20 25 3imtr4i ⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } → 𝑧 ∈ { 𝑥 ∈ { 𝑧 } ∣ 𝜑 } )
27 26 ne0d ⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } → { 𝑥 ∈ { 𝑧 } ∣ 𝜑 } ≠ ∅ )
28 rabn0 ⊢ ( { 𝑥 ∈ { 𝑧 } ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∈ { 𝑧 } 𝜑 )
29 27 28 sylib ⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } → ∃ 𝑥 ∈ { 𝑧 } 𝜑 )
30 vsnex ⊢ { 𝑧 } ∈ V
31 sseq1 ⊢ ( 𝑦 = { 𝑧 } → ( 𝑦 ⊆ 𝐴 ↔ { 𝑧 } ⊆ 𝐴 ) )
32 rexeq ⊢ ( 𝑦 = { 𝑧 } → ( ∃ 𝑥 ∈ 𝑦 𝜑 ↔ ∃ 𝑥 ∈ { 𝑧 } 𝜑 ) )
33 31 32 anbi12d ⊢ ( 𝑦 = { 𝑧 } → ( ( 𝑦 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝑦 𝜑 ) ↔ ( { 𝑧 } ⊆ 𝐴 ∧ ∃ 𝑥 ∈ { 𝑧 } 𝜑 ) ) )
34 30 33 spcev ⊢ ( ( { 𝑧 } ⊆ 𝐴 ∧ ∃ 𝑥 ∈ { 𝑧 } 𝜑 ) → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝑦 𝜑 ) )
35 11 29 34 syl2anc ⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝑦 𝜑 ) )
36 35 exlimiv ⊢ ( ∃ 𝑧 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝑦 𝜑 ) )
37 5 36 sylbi ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝑦 𝜑 ) )