Metamath Proof Explorer

Theorem sbc2or

Description: The disjunction of two equivalences for class substitution does not require a class existence hypothesis. This theorem tells us that there are only 2 possibilities for [ A / x ] ph behavior at proper classes, matching the sbc5 (false) and sbc6 (true) conclusions. This is interesting since dfsbcq and dfsbcq2 (from which it is derived) do not appear to say anything obvious about proper class behavior. Note that this theorem does not tell us that it is always one or the other at proper classes; it could "flip" between false (the first disjunct) and true (the second disjunct) as a function of some other variable y that ph or A may contain. (Contributed by NM, 11-Oct-2004) (Proof modification is discouraged.)

Ref Expression
Assertion sbc2or ( ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) ∨ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 dfsbcq2 ⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
2 eqeq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝐴 ) )
3 2 anbi1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
4 3 exbidv ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
5 sb5 ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )
6 1 4 5 vtoclbg ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
7 6 orcd ⊢ ( 𝐴 ∈ V → ( ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) ∨ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) ) )
8 pm5.15 ⊢ ( ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) ∨ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ¬ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
9 vex ⊢ 𝑥 ∈ V
10 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ V ↔ 𝐴 ∈ V ) )
11 9 10 mpbii ⊢ ( 𝑥 = 𝐴 → 𝐴 ∈ V )
12 11 adantr ⊢ ( ( 𝑥 = 𝐴 ∧ 𝜑 ) → 𝐴 ∈ V )
13 12 con3i ⊢ ( ¬ 𝐴 ∈ V → ¬ ( 𝑥 = 𝐴 ∧ 𝜑 ) )
14 13 nexdv ⊢ ( ¬ 𝐴 ∈ V → ¬ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
15 11 con3i ⊢ ( ¬ 𝐴 ∈ V → ¬ 𝑥 = 𝐴 )
16 15 pm2.21d ⊢ ( ¬ 𝐴 ∈ V → ( 𝑥 = 𝐴 → 𝜑 ) )
17 16 alrimiv ⊢ ( ¬ 𝐴 ∈ V → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) )
18 14 17 2thd ⊢ ( ¬ 𝐴 ∈ V → ( ¬ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) )
19 18 bibi2d ⊢ ( ¬ 𝐴 ∈ V → ( ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ¬ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) ) )
20 19 orbi2d ⊢ ( ¬ 𝐴 ∈ V → ( ( ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) ∨ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ¬ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) ) ↔ ( ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) ∨ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) ) ) )
21 8 20 mpbii ⊢ ( ¬ 𝐴 ∈ V → ( ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) ∨ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) ) )
22 7 21 pm2.61i ⊢ ( ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) ∨ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) )