Proof of Theorem elabgt
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elab6g 3668 | . . 3
⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))) | 
| 2 | 1 | adantr 480 | . 2
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))) | 
| 3 |  | elisset 2822 | . . . . . 6
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴) | 
| 4 |  | biimp 215 | . . . . . . . . 9
⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) | 
| 5 | 4 | imim3i 64 | . . . . . . . 8
⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → ((𝑥 = 𝐴 → 𝜑) → (𝑥 = 𝐴 → 𝜓))) | 
| 6 | 5 | al2imi 1814 | . . . . . . 7
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (∀𝑥(𝑥 = 𝐴 → 𝜑) → ∀𝑥(𝑥 = 𝐴 → 𝜓))) | 
| 7 |  | 19.23v 1941 | . . . . . . 7
⊢
(∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓)) | 
| 8 | 6, 7 | imbitrdi 251 | . . . . . 6
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (∀𝑥(𝑥 = 𝐴 → 𝜑) → (∃𝑥 𝑥 = 𝐴 → 𝜓))) | 
| 9 | 3, 8 | syl7 74 | . . . . 5
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (∀𝑥(𝑥 = 𝐴 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓))) | 
| 10 | 9 | com3r 87 | . . . 4
⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (∀𝑥(𝑥 = 𝐴 → 𝜑) → 𝜓))) | 
| 11 | 10 | imp 406 | . . 3
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (∀𝑥(𝑥 = 𝐴 → 𝜑) → 𝜓)) | 
| 12 |  | biimpr 220 | . . . . . . . 8
⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑)) | 
| 13 | 12 | imim2i 16 | . . . . . . 7
⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝑥 = 𝐴 → (𝜓 → 𝜑))) | 
| 14 | 13 | com23 86 | . . . . . 6
⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝜓 → (𝑥 = 𝐴 → 𝜑))) | 
| 15 | 14 | alimi 1810 | . . . . 5
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → ∀𝑥(𝜓 → (𝑥 = 𝐴 → 𝜑))) | 
| 16 |  | 19.21v 1938 | . . . . 5
⊢
(∀𝑥(𝜓 → (𝑥 = 𝐴 → 𝜑)) ↔ (𝜓 → ∀𝑥(𝑥 = 𝐴 → 𝜑))) | 
| 17 | 15, 16 | sylib 218 | . . . 4
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝜓 → ∀𝑥(𝑥 = 𝐴 → 𝜑))) | 
| 18 | 17 | adantl 481 | . . 3
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝜓 → ∀𝑥(𝑥 = 𝐴 → 𝜑))) | 
| 19 | 11, 18 | impbid 212 | . 2
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | 
| 20 | 2, 19 | bitrd 279 | 1
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |