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

Metamath Proof Explorer

Theorem tz6.12i

Description: Corollary of Theorem 6.12(2) of TakeutiZaring p. 27. (Contributed by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion tz6.12i ⊢ B ≠ ∅ → F ⁡ A = B → A F B

Proof

Step Hyp Ref Expression
1 fvex ⊢ F ⁡ A ∈ V
2 neeq1 ⊢ F ⁡ A = y → F ⁡ A ≠ ∅ ↔ y ≠ ∅
3 tz6.12-2 ⊢ ¬ ∃! y A F y → F ⁡ A = ∅
4 3 necon1ai ⊢ F ⁡ A ≠ ∅ → ∃! y A F y
5 tz6.12c ⊢ ∃! y A F y → F ⁡ A = y ↔ A F y
6 4 5 syl ⊢ F ⁡ A ≠ ∅ → F ⁡ A = y ↔ A F y
7 6 biimpcd ⊢ F ⁡ A = y → F ⁡ A ≠ ∅ → A F y
8 2 7 sylbird ⊢ F ⁡ A = y → y ≠ ∅ → A F y
9 8 eqcoms ⊢ y = F ⁡ A → y ≠ ∅ → A F y
10 neeq1 ⊢ y = F ⁡ A → y ≠ ∅ ↔ F ⁡ A ≠ ∅
11 breq2 ⊢ y = F ⁡ A → A F y ↔ A F F ⁡ A
12 9 10 11 3imtr3d ⊢ y = F ⁡ A → F ⁡ A ≠ ∅ → A F F ⁡ A
13 1 12 vtocle ⊢ F ⁡ A ≠ ∅ → A F F ⁡ A
14 13 a1i ⊢ F ⁡ A = B → F ⁡ A ≠ ∅ → A F F ⁡ A
15 neeq1 ⊢ F ⁡ A = B → F ⁡ A ≠ ∅ ↔ B ≠ ∅
16 breq2 ⊢ F ⁡ A = B → A F F ⁡ A ↔ A F B
17 14 15 16 3imtr3d ⊢ F ⁡ A = B → B ≠ ∅ → A F B
18 17 com12 ⊢ B ≠ ∅ → F ⁡ A = B → A F B