Step |
Hyp |
Ref |
Expression |
1 |
|
onminsb.1 |
⊢ Ⅎ 𝑥 𝜓 |
2 |
|
onminsb.2 |
⊢ ( 𝑥 = ∩ { 𝑥 ∈ On ∣ 𝜑 } → ( 𝜑 ↔ 𝜓 ) ) |
3 |
|
rabn0 |
⊢ ( { 𝑥 ∈ On ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∈ On 𝜑 ) |
4 |
|
ssrab2 |
⊢ { 𝑥 ∈ On ∣ 𝜑 } ⊆ On |
5 |
|
onint |
⊢ ( ( { 𝑥 ∈ On ∣ 𝜑 } ⊆ On ∧ { 𝑥 ∈ On ∣ 𝜑 } ≠ ∅ ) → ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ { 𝑥 ∈ On ∣ 𝜑 } ) |
6 |
4 5
|
mpan |
⊢ ( { 𝑥 ∈ On ∣ 𝜑 } ≠ ∅ → ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ { 𝑥 ∈ On ∣ 𝜑 } ) |
7 |
3 6
|
sylbir |
⊢ ( ∃ 𝑥 ∈ On 𝜑 → ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ { 𝑥 ∈ On ∣ 𝜑 } ) |
8 |
|
nfrab1 |
⊢ Ⅎ 𝑥 { 𝑥 ∈ On ∣ 𝜑 } |
9 |
8
|
nfint |
⊢ Ⅎ 𝑥 ∩ { 𝑥 ∈ On ∣ 𝜑 } |
10 |
|
nfcv |
⊢ Ⅎ 𝑥 On |
11 |
9 10 1 2
|
elrabf |
⊢ ( ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ { 𝑥 ∈ On ∣ 𝜑 } ↔ ( ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ On ∧ 𝜓 ) ) |
12 |
11
|
simprbi |
⊢ ( ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ { 𝑥 ∈ On ∣ 𝜑 } → 𝜓 ) |
13 |
7 12
|
syl |
⊢ ( ∃ 𝑥 ∈ On 𝜑 → 𝜓 ) |