ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  csbiebt GIF version

Theorem csbiebt 3096
Description: Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 3100.) (Contributed by NM, 11-Nov-2005.)
Assertion
Ref Expression
csbiebt ((𝐴𝑉𝑥𝐶) → (∀𝑥(𝑥 = 𝐴𝐵 = 𝐶) ↔ 𝐴 / 𝑥𝐵 = 𝐶))
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝑉(𝑥)

Proof of Theorem csbiebt
StepHypRef Expression
1 elex 2748 . 2 (𝐴𝑉𝐴 ∈ V)
2 spsbc 2974 . . . . 5 (𝐴 ∈ V → (∀𝑥(𝑥 = 𝐴𝐵 = 𝐶) → [𝐴 / 𝑥](𝑥 = 𝐴𝐵 = 𝐶)))
32adantr 276 . . . 4 ((𝐴 ∈ V ∧ 𝑥𝐶) → (∀𝑥(𝑥 = 𝐴𝐵 = 𝐶) → [𝐴 / 𝑥](𝑥 = 𝐴𝐵 = 𝐶)))
4 simpl 109 . . . . 5 ((𝐴 ∈ V ∧ 𝑥𝐶) → 𝐴 ∈ V)
5 biimt 241 . . . . . . 7 (𝑥 = 𝐴 → (𝐵 = 𝐶 ↔ (𝑥 = 𝐴𝐵 = 𝐶)))
6 csbeq1a 3066 . . . . . . . 8 (𝑥 = 𝐴𝐵 = 𝐴 / 𝑥𝐵)
76eqeq1d 2186 . . . . . . 7 (𝑥 = 𝐴 → (𝐵 = 𝐶𝐴 / 𝑥𝐵 = 𝐶))
85, 7bitr3d 190 . . . . . 6 (𝑥 = 𝐴 → ((𝑥 = 𝐴𝐵 = 𝐶) ↔ 𝐴 / 𝑥𝐵 = 𝐶))
98adantl 277 . . . . 5 (((𝐴 ∈ V ∧ 𝑥𝐶) ∧ 𝑥 = 𝐴) → ((𝑥 = 𝐴𝐵 = 𝐶) ↔ 𝐴 / 𝑥𝐵 = 𝐶))
10 nfv 1528 . . . . . 6 𝑥 𝐴 ∈ V
11 nfnfc1 2322 . . . . . 6 𝑥𝑥𝐶
1210, 11nfan 1565 . . . . 5 𝑥(𝐴 ∈ V ∧ 𝑥𝐶)
13 nfcsb1v 3090 . . . . . . 7 𝑥𝐴 / 𝑥𝐵
1413a1i 9 . . . . . 6 ((𝐴 ∈ V ∧ 𝑥𝐶) → 𝑥𝐴 / 𝑥𝐵)
15 simpr 110 . . . . . 6 ((𝐴 ∈ V ∧ 𝑥𝐶) → 𝑥𝐶)
1614, 15nfeqd 2334 . . . . 5 ((𝐴 ∈ V ∧ 𝑥𝐶) → Ⅎ𝑥𝐴 / 𝑥𝐵 = 𝐶)
174, 9, 12, 16sbciedf 2998 . . . 4 ((𝐴 ∈ V ∧ 𝑥𝐶) → ([𝐴 / 𝑥](𝑥 = 𝐴𝐵 = 𝐶) ↔ 𝐴 / 𝑥𝐵 = 𝐶))
183, 17sylibd 149 . . 3 ((𝐴 ∈ V ∧ 𝑥𝐶) → (∀𝑥(𝑥 = 𝐴𝐵 = 𝐶) → 𝐴 / 𝑥𝐵 = 𝐶))
1913a1i 9 . . . . . . . 8 (𝑥𝐶𝑥𝐴 / 𝑥𝐵)
20 id 19 . . . . . . . 8 (𝑥𝐶𝑥𝐶)
2119, 20nfeqd 2334 . . . . . . 7 (𝑥𝐶 → Ⅎ𝑥𝐴 / 𝑥𝐵 = 𝐶)
2211, 21nfan1 1564 . . . . . 6 𝑥(𝑥𝐶𝐴 / 𝑥𝐵 = 𝐶)
237biimprcd 160 . . . . . . 7 (𝐴 / 𝑥𝐵 = 𝐶 → (𝑥 = 𝐴𝐵 = 𝐶))
2423adantl 277 . . . . . 6 ((𝑥𝐶𝐴 / 𝑥𝐵 = 𝐶) → (𝑥 = 𝐴𝐵 = 𝐶))
2522, 24alrimi 1522 . . . . 5 ((𝑥𝐶𝐴 / 𝑥𝐵 = 𝐶) → ∀𝑥(𝑥 = 𝐴𝐵 = 𝐶))
2625ex 115 . . . 4 (𝑥𝐶 → (𝐴 / 𝑥𝐵 = 𝐶 → ∀𝑥(𝑥 = 𝐴𝐵 = 𝐶)))
2726adantl 277 . . 3 ((𝐴 ∈ V ∧ 𝑥𝐶) → (𝐴 / 𝑥𝐵 = 𝐶 → ∀𝑥(𝑥 = 𝐴𝐵 = 𝐶)))
2818, 27impbid 129 . 2 ((𝐴 ∈ V ∧ 𝑥𝐶) → (∀𝑥(𝑥 = 𝐴𝐵 = 𝐶) ↔ 𝐴 / 𝑥𝐵 = 𝐶))
291, 28sylan 283 1 ((𝐴𝑉𝑥𝐶) → (∀𝑥(𝑥 = 𝐴𝐵 = 𝐶) ↔ 𝐴 / 𝑥𝐵 = 𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  wal 1351   = wceq 1353  wcel 2148  wnfc 2306  Vcvv 2737  [wsbc 2962  csb 3057
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-sbc 2963  df-csb 3058
This theorem is referenced by:  csbiedf  3097  csbieb  3098  csbiegf  3100
  Copyright terms: Public domain W3C validator