Theorem sbc2or 1454

Description: The disjunction of two equivalences for class substitution does not require a class existence hypothesis.

Assertion

Ref	Expression
sbc2or	⊢ (([A / x]φ ↔ ∃x(x = A ∧ φ)) ∨ ([A / x]φ ↔ ∀x(x = A → φ)))

Distinct variable group(s):   x,A

Proof of Theorem sbc2or

Step	Hyp	Ref	Expression
1		sbc5g 1450	. . 3 ⊢ (A ∈ V → ([A / x]φ ↔ ∃x(x = A ∧ φ)))
2		orc 225	. . 3 ⊢ (([A / x]φ ↔ ∃x(x = A ∧ φ)) → (([A / x]φ ↔ ∃x(x = A ∧ φ)) ∨ ([A / x]φ ↔ ∀x(x = A → φ))))
3	1, 2	syl 12	. 2 ⊢ (A ∈ V → (([A / x]φ ↔ ∃x(x = A ∧ φ)) ∨ ([A / x]φ ↔ ∀x(x = A → φ))))
4		exmid 494	. . . 4 ⊢ (([A / x]φ ↔ ∃x(x = A ∧ φ)) ∨ ¬ ([A / x]φ ↔ ∃x(x = A ∧ φ)))
5		pm5.18 497	. . . . . 6 ⊢ (([A / x]φ ↔ ∃x(x = A ∧ φ)) ↔ ¬ ([A / x]φ ↔ ¬ ∃x(x = A ∧ φ)))
6	5	bicon2i 194	. . . . 5 ⊢ (([A / x]φ ↔ ¬ ∃x(x = A ∧ φ)) ↔ ¬ ([A / x]φ ↔ ∃x(x = A ∧ φ)))
7	6	orbi2i 214	. . . 4 ⊢ ((([A / x]φ ↔ ∃x(x = A ∧ φ)) ∨ ([A / x]φ ↔ ¬ ∃x(x = A ∧ φ))) ↔ (([A / x]φ ↔ ∃x(x = A ∧ φ)) ∨ ¬ ([A / x]φ ↔ ∃x(x = A ∧ φ))))
8	4, 7	mpbir 165	. . 3 ⊢ (([A / x]φ ↔ ∃x(x = A ∧ φ)) ∨ ([A / x]φ ↔ ¬ ∃x(x = A ∧ φ)))
9		pm5.1 501	. . . . . 6 ⊢ ((¬ ∃x(x = A ∧ φ) ∧ ∀x(x = A → φ)) → (¬ ∃x(x = A ∧ φ) ↔ ∀x(x = A → φ)))
10		visset 1350	. . . . . . . . . 10 ⊢ x ∈ V
11		eleq1 1149	. . . . . . . . . 10 ⊢ (x = A → (x ∈ V ↔ A ∈ V))
12	10, 11	mpbii 168	. . . . . . . . 9 ⊢ (x = A → A ∈ V)
13	12	adantr 306	. . . . . . . 8 ⊢ ((x = A ∧ φ) → A ∈ V)
14	13	con3i 90	. . . . . . 7 ⊢ (¬ A ∈ V → ¬ (x = A ∧ φ))
15	14	nexdv 983	. . . . . 6 ⊢ (¬ A ∈ V → ¬ ∃x(x = A ∧ φ))
16	12	con3i 90	. . . . . . . 8 ⊢ (¬ A ∈ V → ¬ x = A)
17	16	pm2.21d 74	. . . . . . 7 ⊢ (¬ A ∈ V → (x = A → φ))
18	17	19.21aiv 943	. . . . . 6 ⊢ (¬ A ∈ V → ∀x(x = A → φ))
19	9, 15, 18	sylanc 361	. . . . 5 ⊢ (¬ A ∈ V → (¬ ∃x(x = A ∧ φ) ↔ ∀x(x = A → φ)))
20	19	bibi2d 470	. . . 4 ⊢ (¬ A ∈ V → (([A / x]φ ↔ ¬ ∃x(x = A ∧ φ)) ↔ ([A / x]φ ↔ ∀x(x = A → φ))))
21	20	orbi2d 466	. . 3 ⊢ (¬ A ∈ V → ((([A / x]φ ↔ ∃x(x = A ∧ φ)) ∨ ([A / x]φ ↔ ¬ ∃x(x = A ∧ φ))) ↔ (([A / x]φ ↔ ∃x(x = A ∧ φ)) ∨ ([A / x]φ ↔ ∀x(x = A → φ)))))
22	8, 21	mpbii 168	. 2 ⊢ (¬ A ∈ V → (([A / x]φ ↔ ∃x(x = A ∧ φ)) ∨ ([A / x]φ ↔ ∀x(x = A → φ))))
23	3, 22	pm2.61i 110	1 ⊢ (([A / x]φ ↔ ∃x(x = A ∧ φ)) ∨ ([A / x]φ ↔ ∀x(x = A → φ)))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∨ wo 195   ∧ wa 196  ∀wal 672  ∃wex 678   = wceq 1091   ∈ wcel 1092  Vcvv 1348  [wsbc 1440

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-sbc 1441

metamath.org