Metamath Proof Explorer

Theorem e2ebindVD

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 ) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. e2ebind is e2ebindVD without virtual deductions and was automatically derived from e2ebindVD .

1:: |- ( ph <-> ph )
2:1: |- ( A. y y = x -> ( ph <-> ph ) )
3:2: |- ( A. y y = x -> ( E. y ph <-> E. x ph ) )
4:: |- (. A. y y = x ->. A. y y = x ).
5:3,4: |- (. A. y y = x ->. ( E. y ph <-> E. x ph ) ).
6:: |- ( A. y y = x -> A. y A. y y = x )
7:5,6: |- (. A. y y = x ->. A. y ( E. y ph <-> E. x ph ) ).
8:7: |- (. A. y y = x ->. ( E. y E. y ph <-> E. y E. x ph ) ).
9:: |- ( E. y E. x ph <-> E. x E. y ph )
10:8,9: |- (. A. y y = x ->. ( E. y E. y ph <-> E. x E. y ph ) ).
11:: |- ( E. y ph -> A. y E. y ph )
12:11: |- ( E. y E. y ph <-> E. y ph )
13:10,12: |- (. A. y y = x ->. ( E. x E. y ph <-> E. y ph ) ).
14:13: |- ( A. y y = x -> ( E. x E. y ph <-> E. y ph ) )
15:: |- ( A. y y = x <-> A. x x = y )
qed:14,15: |- ( A. x x = y -> ( E. x E. y ph <-> E. y ph ) )
(Contributed by Alan Sare, 27-Nov-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion e2ebindVD ⊢∀xx=y→∃x∃yφ↔∃yφ

Proof

Step Hyp Ref Expression
1 axc11n ⊢∀xx=y→∀yy=x
2 hba1 ⊢∀yy=x→∀y∀yy=x
3 idn1 ⊢∀yy=x→∀yy=x
4 biid ⊢φ↔φ
5 4 a1i ⊢∀yy=x→φ↔φ
6 5 drex1 ⊢∀yy=x→∃yφ↔∃xφ
7 3 6 e1a ⊢∀yy=x→∃yφ↔∃xφ
8 2 7 gen11nv ⊢∀yy=x→∀y∃yφ↔∃xφ
9 exbi ⊢∀y∃yφ↔∃xφ→∃y∃yφ↔∃y∃xφ
10 8 9 e1a ⊢∀yy=x→∃y∃yφ↔∃y∃xφ
11 excom ⊢∃y∃xφ↔∃x∃yφ
12 bibi1 ⊢∃y∃yφ↔∃y∃xφ→∃y∃yφ↔∃x∃yφ↔∃y∃xφ↔∃x∃yφ
13 12 biimprd ⊢∃y∃yφ↔∃y∃xφ→∃y∃xφ↔∃x∃yφ→∃y∃yφ↔∃x∃yφ
14 10 11 13 e10 ⊢∀yy=x→∃y∃yφ↔∃x∃yφ
15 nfe1 ⊢Ⅎy∃yφ
16 15 19.9 ⊢∃y∃yφ↔∃yφ
17 bitr3 ⊢∃y∃yφ↔∃x∃yφ→∃y∃yφ↔∃yφ→∃x∃yφ↔∃yφ
18 14 16 17 e10 ⊢∀yy=x→∃x∃yφ↔∃yφ
19 18 in1 ⊢∀yy=x→∃x∃yφ↔∃yφ
20 1 19 syl ⊢∀xx=y→∃x∃yφ↔∃yφ