Metamath Proof Explorer

Theorem sbcrext

Description: Interchange class substitution and restricted existential quantifier. (Contributed by NM, 1-Mar-2008) (Proof shortened by Mario Carneiro, 13-Oct-2016) (Revised by NM, 18-Aug-2018) (Proof shortened by JJ, 7-Jul-2021)

Ref Expression
Assertion sbcrext ( Ⅎ 𝑦 𝐴 → ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) )

Proof

Step Hyp Ref Expression
1 sbcex ⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ∈ 𝐵 𝜑 → 𝐴 ∈ V )
2 1 a1i ⊢ ( Ⅎ 𝑦 𝐴 → ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ∈ 𝐵 𝜑 → 𝐴 ∈ V ) )
3 nfnfc1 ⊢ Ⅎ 𝑦 Ⅎ 𝑦 𝐴
4 id ⊢ ( Ⅎ 𝑦 𝐴 → Ⅎ 𝑦 𝐴 )
5 nfcvd ⊢ ( Ⅎ 𝑦 𝐴 → Ⅎ 𝑦 V )
6 4 5 nfeld ⊢ ( Ⅎ 𝑦 𝐴 → Ⅎ 𝑦 𝐴 ∈ V )
7 sbcex ⊢ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 ∈ V )
8 7 2a1i ⊢ ( Ⅎ 𝑦 𝐴 → ( 𝑦 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 ∈ V ) ) )
9 3 6 8 rexlimd2 ⊢ ( Ⅎ 𝑦 𝐴 → ( ∃ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 ∈ V ) )
10 sbcng ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 ¬ 𝜑 ) )
11 10 adantl ⊢ ( ( Ⅎ 𝑦 𝐴 ∧ 𝐴 ∈ V ) → ( [ 𝐴 / 𝑥 ] ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 ¬ 𝜑 ) )
12 sbcralt ⊢ ( ( 𝐴 ∈ V ∧ Ⅎ 𝑦 𝐴 ) → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] ¬ 𝜑 ) )
13 12 ancoms ⊢ ( ( Ⅎ 𝑦 𝐴 ∧ 𝐴 ∈ V ) → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] ¬ 𝜑 ) )
14 3 6 nfan1 ⊢ Ⅎ 𝑦 ( Ⅎ 𝑦 𝐴 ∧ 𝐴 ∈ V )
15 sbcng ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] ¬ 𝜑 ↔ ¬ [ 𝐴 / 𝑥 ] 𝜑 ) )
16 15 adantl ⊢ ( ( Ⅎ 𝑦 𝐴 ∧ 𝐴 ∈ V ) → ( [ 𝐴 / 𝑥 ] ¬ 𝜑 ↔ ¬ [ 𝐴 / 𝑥 ] 𝜑 ) )
17 14 16 ralbid ⊢ ( ( Ⅎ 𝑦 𝐴 ∧ 𝐴 ∈ V ) → ( ∀ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] ¬ 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 ¬ [ 𝐴 / 𝑥 ] 𝜑 ) )
18 13 17 bitrd ⊢ ( ( Ⅎ 𝑦 𝐴 ∧ 𝐴 ∈ V ) → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 ¬ [ 𝐴 / 𝑥 ] 𝜑 ) )
19 18 notbid ⊢ ( ( Ⅎ 𝑦 𝐴 ∧ 𝐴 ∈ V ) → ( ¬ [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀ 𝑦 ∈ 𝐵 ¬ [ 𝐴 / 𝑥 ] 𝜑 ) )
20 11 19 bitrd ⊢ ( ( Ⅎ 𝑦 𝐴 ∧ 𝐴 ∈ V ) → ( [ 𝐴 / 𝑥 ] ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀ 𝑦 ∈ 𝐵 ¬ [ 𝐴 / 𝑥 ] 𝜑 ) )
21 dfrex2 ⊢ ( ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝜑 )
22 21 sbcbii ⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ∈ 𝐵 𝜑 ↔ [ 𝐴 / 𝑥 ] ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝜑 )
23 dfrex2 ⊢ ( ∃ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ↔ ¬ ∀ 𝑦 ∈ 𝐵 ¬ [ 𝐴 / 𝑥 ] 𝜑 )
24 20 22 23 3bitr4g ⊢ ( ( Ⅎ 𝑦 𝐴 ∧ 𝐴 ∈ V ) → ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) )
25 24 ex ⊢ ( Ⅎ 𝑦 𝐴 → ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) ) )
26 2 9 25 pm5.21ndd ⊢ ( Ⅎ 𝑦 𝐴 → ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) )