MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opelopabsb Structured version   Visualization version   GIF version

Theorem opelopabsb 5398
Description: The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)
Assertion
Ref Expression
opelopabsb (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)
Distinct variable groups:   𝑥,𝑦   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑦)

Proof of Theorem opelopabsb
Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3482 . . . . . . . . . 10 𝑥 ∈ V
2 vex 3482 . . . . . . . . . 10 𝑦 ∈ V
31, 2opnzi 5347 . . . . . . . . 9 𝑥, 𝑦⟩ ≠ ∅
4 simpl 486 . . . . . . . . . . 11 ((∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∅ = ⟨𝑥, 𝑦⟩)
54eqcomd 2830 . . . . . . . . . 10 ((∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ⟨𝑥, 𝑦⟩ = ∅)
65necon3ai 3038 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ≠ ∅ → ¬ (∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
73, 6ax-mp 5 . . . . . . . 8 ¬ (∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
87nex 1802 . . . . . . 7 ¬ ∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
98nex 1802 . . . . . 6 ¬ ∃𝑥𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
10 elopab 5395 . . . . . 6 (∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
119, 10mtbir 326 . . . . 5 ¬ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}
12 eleq1 2903 . . . . 5 (⟨𝐴, 𝐵⟩ = ∅ → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}))
1311, 12mtbiri 330 . . . 4 (⟨𝐴, 𝐵⟩ = ∅ → ¬ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
1413necon2ai 3042 . . 3 (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → ⟨𝐴, 𝐵⟩ ≠ ∅)
15 opnz 5346 . . 3 (⟨𝐴, 𝐵⟩ ≠ ∅ ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V))
1614, 15sylib 221 . 2 (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → (𝐴 ∈ V ∧ 𝐵 ∈ V))
17 sbcex 3767 . . 3 ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑𝐴 ∈ V)
18 spesbc 3848 . . . 4 ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → ∃𝑥[𝐵 / 𝑦]𝜑)
19 sbcex 3767 . . . . 5 ([𝐵 / 𝑦]𝜑𝐵 ∈ V)
2019exlimiv 1932 . . . 4 (∃𝑥[𝐵 / 𝑦]𝜑𝐵 ∈ V)
2118, 20syl 17 . . 3 ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑𝐵 ∈ V)
2217, 21jca 515 . 2 ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
23 opeq1 4784 . . . . 5 (𝑧 = 𝐴 → ⟨𝑧, 𝑤⟩ = ⟨𝐴, 𝑤⟩)
2423eleq1d 2900 . . . 4 (𝑧 = 𝐴 → (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}))
25 dfsbcq2 3760 . . . 4 (𝑧 = 𝐴 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑[𝐴 / 𝑥][𝑤 / 𝑦]𝜑))
2624, 25bibi12d 349 . . 3 (𝑧 = 𝐴 → ((⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) ↔ (⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝑤 / 𝑦]𝜑)))
27 opeq2 4785 . . . . 5 (𝑤 = 𝐵 → ⟨𝐴, 𝑤⟩ = ⟨𝐴, 𝐵⟩)
2827eleq1d 2900 . . . 4 (𝑤 = 𝐵 → (⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}))
29 dfsbcq2 3760 . . . . 5 (𝑤 = 𝐵 → ([𝑤 / 𝑦]𝜑[𝐵 / 𝑦]𝜑))
3029sbcbidv 3811 . . . 4 (𝑤 = 𝐵 → ([𝐴 / 𝑥][𝑤 / 𝑦]𝜑[𝐴 / 𝑥][𝐵 / 𝑦]𝜑))
3128, 30bibi12d 349 . . 3 (𝑤 = 𝐵 → ((⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝑤 / 𝑦]𝜑) ↔ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)))
32 nfopab1 5116 . . . . . 6 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}
3332nfel2 2998 . . . . 5 𝑥𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}
34 nfs1v 2161 . . . . 5 𝑥[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
3533, 34nfbi 1905 . . . 4 𝑥(⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
36 opeq1 4784 . . . . . 6 (𝑥 = 𝑧 → ⟨𝑥, 𝑤⟩ = ⟨𝑧, 𝑤⟩)
3736eleq1d 2900 . . . . 5 (𝑥 = 𝑧 → (⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}))
38 sbequ12 2255 . . . . 5 (𝑥 = 𝑧 → ([𝑤 / 𝑦]𝜑 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
3937, 38bibi12d 349 . . . 4 (𝑥 = 𝑧 → ((⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑) ↔ (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)))
40 nfopab2 5117 . . . . . . 7 𝑦{⟨𝑥, 𝑦⟩ ∣ 𝜑}
4140nfel2 2998 . . . . . 6 𝑦𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}
42 nfs1v 2161 . . . . . 6 𝑦[𝑤 / 𝑦]𝜑
4341, 42nfbi 1905 . . . . 5 𝑦(⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑)
44 opeq2 4785 . . . . . . 7 (𝑦 = 𝑤 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑤⟩)
4544eleq1d 2900 . . . . . 6 (𝑦 = 𝑤 → (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}))
46 sbequ12 2255 . . . . . 6 (𝑦 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑦]𝜑))
4745, 46bibi12d 349 . . . . 5 (𝑦 = 𝑤 → ((⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑) ↔ (⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑)))
48 opabidw 5393 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
4943, 47, 48chvarfv 2244 . . . 4 (⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑)
5035, 39, 49chvarfv 2244 . . 3 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
5126, 31, 50vtocl2g 3557 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑))
5216, 22, 51pm5.21nii 383 1 (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209  wa 399   = wceq 1538  wex 1781  [wsb 2070  wcel 2115  wne 3013  Vcvv 3479  [wsbc 3757  c0 4274  cop 4554  {copab 5109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5184  ax-nul 5191  ax-pr 5311
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-ral 3137  df-rex 3138  df-rab 3141  df-v 3481  df-sbc 3758  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-sn 4549  df-pr 4551  df-op 4555  df-opab 5110
This theorem is referenced by:  brabsb  5399  opelopabgf  5408  opelopabaf  5412  opelopabf  5413  difopab  5683  isarep1  6423  fmptsnd  6912
  Copyright terms: Public domain W3C validator