![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > opabidw | Structured version Visualization version GIF version |
Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 5525 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by NM, 14-Apr-1995.) Avoid ax-13 2370. (Revised by Gino Giotto, 26-Jan-2024.) |
Ref | Expression |
---|---|
opabidw | ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opex 5464 | . 2 ⊢ ⟨𝑥, 𝑦⟩ ∈ V | |
2 | copsexgw 5490 | . . 3 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))) | |
3 | 2 | bicomd 222 | . 2 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜑)) |
4 | df-opab 5211 | . 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} | |
5 | 1, 3, 4 | elab2 3672 | 1 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 395 = wceq 1540 ∃wex 1780 ∈ wcel 2105 ⟨cop 4634 {copab 5210 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-opab 5211 |
This theorem is referenced by: rexopabb 5528 ssopab2bw 5547 dmopab 5915 rnopab 5953 funopab 6583 opabiota 6974 fvopab5 7030 f1ompt 7112 ovid 7552 zfrep6 7944 enssdom 8976 omxpenlem 9076 infxpenlem 10011 canthwelem 10648 pospo 18303 2ndcdisj 23181 lgsquadlem1 27120 lgsquadlem2 27121 h2hlm 30501 opabdm 32108 opabrn 32109 fpwrelmap 32226 eulerpartlemgvv 33674 fineqvrep 34394 satfvsucsuc 34655 bj-opelopabid 36372 phpreu 36776 poimirlem26 36818 vvdifopab 37432 brabidgaw 37538 diclspsn 40369 areaquad 42268 sprsymrelf 46462 |
Copyright terms: Public domain | W3C validator |