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

Theorem opelopabsb 4947
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 3189 . . . . . . . . . 10 𝑥 ∈ V
2 vex 3189 . . . . . . . . . 10 𝑦 ∈ V
31, 2opnzi 4905 . . . . . . . . 9 𝑥, 𝑦⟩ ≠ ∅
4 simpl 473 . . . . . . . . . . 11 ((∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∅ = ⟨𝑥, 𝑦⟩)
54eqcomd 2627 . . . . . . . . . 10 ((∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ⟨𝑥, 𝑦⟩ = ∅)
65necon3ai 2815 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ≠ ∅ → ¬ (∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
73, 6ax-mp 5 . . . . . . . 8 ¬ (∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
87nex 1728 . . . . . . 7 ¬ ∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
98nex 1728 . . . . . 6 ¬ ∃𝑥𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
10 elopab 4945 . . . . . 6 (∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
119, 10mtbir 313 . . . . 5 ¬ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}
12 eleq1 2686 . . . . 5 (⟨𝐴, 𝐵⟩ = ∅ → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}))
1311, 12mtbiri 317 . . . 4 (⟨𝐴, 𝐵⟩ = ∅ → ¬ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
1413necon2ai 2819 . . 3 (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → ⟨𝐴, 𝐵⟩ ≠ ∅)
15 opnz 4904 . . 3 (⟨𝐴, 𝐵⟩ ≠ ∅ ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V))
1614, 15sylib 208 . 2 (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → (𝐴 ∈ V ∧ 𝐵 ∈ V))
17 sbcex 3428 . . 3 ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑𝐴 ∈ V)
18 spesbc 3503 . . . 4 ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → ∃𝑥[𝐵 / 𝑦]𝜑)
19 sbcex 3428 . . . . 5 ([𝐵 / 𝑦]𝜑𝐵 ∈ V)
2019exlimiv 1855 . . . 4 (∃𝑥[𝐵 / 𝑦]𝜑𝐵 ∈ V)
2118, 20syl 17 . . 3 ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑𝐵 ∈ V)
2217, 21jca 554 . 2 ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
23 opeq1 4372 . . . . 5 (𝑧 = 𝐴 → ⟨𝑧, 𝑤⟩ = ⟨𝐴, 𝑤⟩)
2423eleq1d 2683 . . . 4 (𝑧 = 𝐴 → (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}))
25 dfsbcq2 3421 . . . 4 (𝑧 = 𝐴 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑[𝐴 / 𝑥][𝑤 / 𝑦]𝜑))
2624, 25bibi12d 335 . . 3 (𝑧 = 𝐴 → ((⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) ↔ (⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝑤 / 𝑦]𝜑)))
27 opeq2 4373 . . . . 5 (𝑤 = 𝐵 → ⟨𝐴, 𝑤⟩ = ⟨𝐴, 𝐵⟩)
2827eleq1d 2683 . . . 4 (𝑤 = 𝐵 → (⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}))
29 dfsbcq2 3421 . . . . 5 (𝑤 = 𝐵 → ([𝑤 / 𝑦]𝜑[𝐵 / 𝑦]𝜑))
3029sbcbidv 3473 . . . 4 (𝑤 = 𝐵 → ([𝐴 / 𝑥][𝑤 / 𝑦]𝜑[𝐴 / 𝑥][𝐵 / 𝑦]𝜑))
3128, 30bibi12d 335 . . 3 (𝑤 = 𝐵 → ((⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝑤 / 𝑦]𝜑) ↔ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)))
32 nfopab1 4683 . . . . . 6 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}
3332nfel2 2777 . . . . 5 𝑥𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}
34 nfs1v 2436 . . . . 5 𝑥[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
3533, 34nfbi 1830 . . . 4 𝑥(⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
36 opeq1 4372 . . . . . 6 (𝑥 = 𝑧 → ⟨𝑥, 𝑤⟩ = ⟨𝑧, 𝑤⟩)
3736eleq1d 2683 . . . . 5 (𝑥 = 𝑧 → (⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}))
38 sbequ12 2108 . . . . 5 (𝑥 = 𝑧 → ([𝑤 / 𝑦]𝜑 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
3937, 38bibi12d 335 . . . 4 (𝑥 = 𝑧 → ((⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑) ↔ (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)))
40 nfopab2 4684 . . . . . . 7 𝑦{⟨𝑥, 𝑦⟩ ∣ 𝜑}
4140nfel2 2777 . . . . . 6 𝑦𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}
42 nfs1v 2436 . . . . . 6 𝑦[𝑤 / 𝑦]𝜑
4341, 42nfbi 1830 . . . . 5 𝑦(⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑)
44 opeq2 4373 . . . . . . 7 (𝑦 = 𝑤 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑤⟩)
4544eleq1d 2683 . . . . . 6 (𝑦 = 𝑤 → (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}))
46 sbequ12 2108 . . . . . 6 (𝑦 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑦]𝜑))
4745, 46bibi12d 335 . . . . 5 (𝑦 = 𝑤 → ((⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑) ↔ (⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑)))
48 opabid 4944 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
4943, 47, 48chvar 2261 . . . 4 (⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑)
5035, 39, 49chvar 2261 . . 3 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
5126, 31, 50vtocl2g 3256 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑))
5216, 22, 51pm5.21nii 368 1 (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 384   = wceq 1480  wex 1701  [wsb 1877  wcel 1987  wne 2790  Vcvv 3186  [wsbc 3418  c0 3893  cop 4156  {copab 4674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4743  ax-nul 4751  ax-pr 4869
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3419  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-sn 4151  df-pr 4153  df-op 4157  df-opab 4676
This theorem is referenced by:  brabsb  4948  opelopabgf  4957  opelopabaf  4961  opelopabf  4962  difopab  5215  isarep1  5937  fmptsnd  6392
  Copyright terms: Public domain W3C validator