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

Theorem opelopabsb 5529
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 3476 . . . . . . . . . 10 𝑥 ∈ V
2 vex 3476 . . . . . . . . . 10 𝑦 ∈ V
31, 2opnzi 5473 . . . . . . . . 9 𝑥, 𝑦⟩ ≠ ∅
4 simpl 481 . . . . . . . . . . 11 ((∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∅ = ⟨𝑥, 𝑦⟩)
54eqcomd 2736 . . . . . . . . . 10 ((∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ⟨𝑥, 𝑦⟩ = ∅)
65necon3ai 2963 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ≠ ∅ → ¬ (∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
73, 6ax-mp 5 . . . . . . . 8 ¬ (∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
87nex 1800 . . . . . . 7 ¬ ∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
98nex 1800 . . . . . 6 ¬ ∃𝑥𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
10 elopab 5526 . . . . . 6 (∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
119, 10mtbir 322 . . . . 5 ¬ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}
12 eleq1 2819 . . . . 5 (⟨𝐴, 𝐵⟩ = ∅ → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}))
1311, 12mtbiri 326 . . . 4 (⟨𝐴, 𝐵⟩ = ∅ → ¬ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
1413necon2ai 2968 . . 3 (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → ⟨𝐴, 𝐵⟩ ≠ ∅)
15 opnz 5472 . . 3 (⟨𝐴, 𝐵⟩ ≠ ∅ ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V))
1614, 15sylib 217 . 2 (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → (𝐴 ∈ V ∧ 𝐵 ∈ V))
17 sbcex 3786 . . 3 ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑𝐴 ∈ V)
18 spesbc 3875 . . . 4 ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → ∃𝑥[𝐵 / 𝑦]𝜑)
19 sbcex 3786 . . . . 5 ([𝐵 / 𝑦]𝜑𝐵 ∈ V)
2019exlimiv 1931 . . . 4 (∃𝑥[𝐵 / 𝑦]𝜑𝐵 ∈ V)
2118, 20syl 17 . . 3 ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑𝐵 ∈ V)
2217, 21jca 510 . 2 ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
23 opeq1 4872 . . . . 5 (𝑧 = 𝐴 → ⟨𝑧, 𝑤⟩ = ⟨𝐴, 𝑤⟩)
2423eleq1d 2816 . . . 4 (𝑧 = 𝐴 → (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}))
25 dfsbcq2 3779 . . . 4 (𝑧 = 𝐴 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑[𝐴 / 𝑥][𝑤 / 𝑦]𝜑))
2624, 25bibi12d 344 . . 3 (𝑧 = 𝐴 → ((⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) ↔ (⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝑤 / 𝑦]𝜑)))
27 opeq2 4873 . . . . 5 (𝑤 = 𝐵 → ⟨𝐴, 𝑤⟩ = ⟨𝐴, 𝐵⟩)
2827eleq1d 2816 . . . 4 (𝑤 = 𝐵 → (⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}))
29 dfsbcq2 3779 . . . . 5 (𝑤 = 𝐵 → ([𝑤 / 𝑦]𝜑[𝐵 / 𝑦]𝜑))
3029sbcbidv 3835 . . . 4 (𝑤 = 𝐵 → ([𝐴 / 𝑥][𝑤 / 𝑦]𝜑[𝐴 / 𝑥][𝐵 / 𝑦]𝜑))
3128, 30bibi12d 344 . . 3 (𝑤 = 𝐵 → ((⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝑤 / 𝑦]𝜑) ↔ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)))
32 vopelopabsb 5528 . . 3 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
3326, 31, 32vtocl2g 3562 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑))
3416, 22, 33pm5.21nii 377 1 (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 394   = wceq 1539  wex 1779  [wsb 2065  wcel 2104  wne 2938  Vcvv 3472  [wsbc 3776  c0 4321  cop 4633  {copab 5209
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-opab 5210
This theorem is referenced by:  brabsb  5530  opelopabgf  5539  opelopabaf  5543  opelopabf  5544  difopabOLD  5830  isarep1OLD  6637  fmptsnd  7168
  Copyright terms: Public domain W3C validator