Step |
Hyp |
Ref |
Expression |
1 |
|
onminex.1 |
⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) |
2 |
|
ssrab2 |
⊢ { 𝑥 ∈ On ∣ 𝜑 } ⊆ On |
3 |
|
rabn0 |
⊢ ( { 𝑥 ∈ On ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∈ On 𝜑 ) |
4 |
3
|
biimpri |
⊢ ( ∃ 𝑥 ∈ On 𝜑 → { 𝑥 ∈ On ∣ 𝜑 } ≠ ∅ ) |
5 |
|
oninton |
⊢ ( ( { 𝑥 ∈ On ∣ 𝜑 } ⊆ On ∧ { 𝑥 ∈ On ∣ 𝜑 } ≠ ∅ ) → ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ On ) |
6 |
2 4 5
|
sylancr |
⊢ ( ∃ 𝑥 ∈ On 𝜑 → ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ On ) |
7 |
|
onminesb |
⊢ ( ∃ 𝑥 ∈ On 𝜑 → [ ∩ { 𝑥 ∈ On ∣ 𝜑 } / 𝑥 ] 𝜑 ) |
8 |
|
onss |
⊢ ( ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ On → ∩ { 𝑥 ∈ On ∣ 𝜑 } ⊆ On ) |
9 |
6 8
|
syl |
⊢ ( ∃ 𝑥 ∈ On 𝜑 → ∩ { 𝑥 ∈ On ∣ 𝜑 } ⊆ On ) |
10 |
9
|
sseld |
⊢ ( ∃ 𝑥 ∈ On 𝜑 → ( 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝜑 } → 𝑦 ∈ On ) ) |
11 |
1
|
onnminsb |
⊢ ( 𝑦 ∈ On → ( 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝜑 } → ¬ 𝜓 ) ) |
12 |
10 11
|
syli |
⊢ ( ∃ 𝑥 ∈ On 𝜑 → ( 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝜑 } → ¬ 𝜓 ) ) |
13 |
12
|
ralrimiv |
⊢ ( ∃ 𝑥 ∈ On 𝜑 → ∀ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝜑 } ¬ 𝜓 ) |
14 |
|
dfsbcq2 |
⊢ ( 𝑧 = ∩ { 𝑥 ∈ On ∣ 𝜑 } → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ ∩ { 𝑥 ∈ On ∣ 𝜑 } / 𝑥 ] 𝜑 ) ) |
15 |
|
raleq |
⊢ ( 𝑧 = ∩ { 𝑥 ∈ On ∣ 𝜑 } → ( ∀ 𝑦 ∈ 𝑧 ¬ 𝜓 ↔ ∀ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝜑 } ¬ 𝜓 ) ) |
16 |
14 15
|
anbi12d |
⊢ ( 𝑧 = ∩ { 𝑥 ∈ On ∣ 𝜑 } → ( ( [ 𝑧 / 𝑥 ] 𝜑 ∧ ∀ 𝑦 ∈ 𝑧 ¬ 𝜓 ) ↔ ( [ ∩ { 𝑥 ∈ On ∣ 𝜑 } / 𝑥 ] 𝜑 ∧ ∀ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝜑 } ¬ 𝜓 ) ) ) |
17 |
16
|
rspcev |
⊢ ( ( ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ On ∧ ( [ ∩ { 𝑥 ∈ On ∣ 𝜑 } / 𝑥 ] 𝜑 ∧ ∀ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝜑 } ¬ 𝜓 ) ) → ∃ 𝑧 ∈ On ( [ 𝑧 / 𝑥 ] 𝜑 ∧ ∀ 𝑦 ∈ 𝑧 ¬ 𝜓 ) ) |
18 |
6 7 13 17
|
syl12anc |
⊢ ( ∃ 𝑥 ∈ On 𝜑 → ∃ 𝑧 ∈ On ( [ 𝑧 / 𝑥 ] 𝜑 ∧ ∀ 𝑦 ∈ 𝑧 ¬ 𝜓 ) ) |
19 |
|
nfv |
⊢ Ⅎ 𝑧 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑥 ¬ 𝜓 ) |
20 |
|
nfs1v |
⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑 |
21 |
|
nfv |
⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝑧 ¬ 𝜓 |
22 |
20 21
|
nfan |
⊢ Ⅎ 𝑥 ( [ 𝑧 / 𝑥 ] 𝜑 ∧ ∀ 𝑦 ∈ 𝑧 ¬ 𝜓 ) |
23 |
|
sbequ12 |
⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) ) |
24 |
|
raleq |
⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝑥 ¬ 𝜓 ↔ ∀ 𝑦 ∈ 𝑧 ¬ 𝜓 ) ) |
25 |
23 24
|
anbi12d |
⊢ ( 𝑥 = 𝑧 → ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑥 ¬ 𝜓 ) ↔ ( [ 𝑧 / 𝑥 ] 𝜑 ∧ ∀ 𝑦 ∈ 𝑧 ¬ 𝜓 ) ) ) |
26 |
19 22 25
|
cbvrexw |
⊢ ( ∃ 𝑥 ∈ On ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑥 ¬ 𝜓 ) ↔ ∃ 𝑧 ∈ On ( [ 𝑧 / 𝑥 ] 𝜑 ∧ ∀ 𝑦 ∈ 𝑧 ¬ 𝜓 ) ) |
27 |
18 26
|
sylibr |
⊢ ( ∃ 𝑥 ∈ On 𝜑 → ∃ 𝑥 ∈ On ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑥 ¬ 𝜓 ) ) |