Theorem sbc2or 1954

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:   x,A

Proof of Theorem sbc2or

Step	Hyp	Ref	Expression
1		sbc5g 1950	. . 3 ⊢ (A ∈ V → ([A / x]φ ↔ ∃x(x = A ⋀ φ)))
2	1	orcd 272	. 2 ⊢ (A ∈ V → (([A / x]φ ↔ ∃x(x = A ⋀ φ)) ⋁ ([A / x]φ ↔ ∀x(x = A → φ))))
3		pm5.15 665	. . 3 ⊢ (([A / x]φ ↔ ∃x(x = A ⋀ φ)) ⋁ ([A / x]φ ↔ ¬ ∃x(x = A ⋀ φ)))
4		pm5.1 675	. . . . . 6 ⊢ ((¬ ∃x(x = A ⋀ φ) ⋀ ∀x(x = A → φ)) → (¬ ∃x(x = A ⋀ φ) ↔ ∀x(x = A → φ)))
5		visset 1809	. . . . . . . . . 10 ⊢ x ∈ V
6		eleq1 1531	. . . . . . . . . 10 ⊢ (x = A → (x ∈ V ↔ A ∈ V))
7	5, 6	mpbii 193	. . . . . . . . 9 ⊢ (x = A → A ∈ V)
8	7	adantr 389	. . . . . . . 8 ⊢ ((x = A ⋀ φ) → A ∈ V)
9	8	con3i 98	. . . . . . 7 ⊢ (¬ A ∈ V → ¬ (x = A ⋀ φ))
10	9	nexdv 1324	. . . . . 6 ⊢ (¬ A ∈ V → ¬ ∃x(x = A ⋀ φ))
11	7	con3i 98	. . . . . . . 8 ⊢ (¬ A ∈ V → ¬ x = A)
12	11	pm2.21d 78	. . . . . . 7 ⊢ (¬ A ∈ V → (x = A → φ))
13	12	19.21aiv 1284	. . . . . 6 ⊢ (¬ A ∈ V → ∀x(x = A → φ))
14	4, 10, 13	sylanc 471	. . . . 5 ⊢ (¬ A ∈ V → (¬ ∃x(x = A ⋀ φ) ↔ ∀x(x = A → φ)))
15	14	bibi2d 617	. . . 4 ⊢ (¬ A ∈ V → (([A / x]φ ↔ ¬ ∃x(x = A ⋀ φ)) ↔ ([A / x]φ ↔ ∀x(x = A → φ))))
16	15	orbi2d 613	. . 3 ⊢ (¬ A ∈ V → ((([A / x]φ ↔ ∃x(x = A ⋀ φ)) ⋁ ([A / x]φ ↔ ¬ ∃x(x = A ⋀ φ))) ↔ (([A / x]φ ↔ ∃x(x = A ⋀ φ)) ⋁ ([A / x]φ ↔ ∀x(x = A → φ)))))
17	3, 16	mpbii 193	. 2 ⊢ (¬ A ∈ V → (([A / x]φ ↔ ∃x(x = A ⋀ φ)) ⋁ ([A / x]φ ↔ ∀x(x = A → φ))))
18	2, 17	pm2.61i 126	1 ⊢ (([A / x]φ ↔ ∃x(x = A ⋀ φ)) ⋁ ([A / x]φ ↔ ∀x(x = A → φ)))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋁ wo 222   ⋀ wa 223  ∀wal 952   = wceq 954   ∈ wcel 956  ∃wex 978  [wsbc 1168  Vcvv 1807

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-sbc 1938

Copyright terms: Public domain