![]() |
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 5438 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 14-Apr-1995.) (Revised by Gino Giotto, 26-Jan-2024.) |
Ref | Expression |
---|---|
opabidw | ⊢ (〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opex 5379 | . 2 ⊢ 〈𝑥, 𝑦〉 ∈ V | |
2 | copsexgw 5404 | . . 3 ⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑))) | |
3 | 2 | bicomd 222 | . 2 ⊢ (𝑧 = 〈𝑥, 𝑦〉 → (∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜑)) |
4 | df-opab 5137 | . 2 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} | |
5 | 1, 3, 4 | elab2 3613 | 1 ⊢ (〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 = wceq 1539 ∃wex 1782 ∈ wcel 2106 〈cop 4567 {copab 5136 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-opab 5137 |
This theorem is referenced by: rexopabb 5441 ssopab2bw 5460 dmopab 5824 rnopab 5863 funopab 6469 opabiota 6851 fvopab5 6907 f1ompt 6985 ovid 7414 zfrep6 7797 enssdom 8765 omxpenlem 8860 infxpenlem 9769 canthwelem 10406 pospo 18063 2ndcdisj 22607 lgsquadlem1 26528 lgsquadlem2 26529 h2hlm 29342 opabdm 30951 opabrn 30952 fpwrelmap 31068 eulerpartlemgvv 32343 fineqvrep 33064 satfvsucsuc 33327 bj-opelopabid 35358 phpreu 35761 poimirlem26 35803 vvdifopab 36399 brabidgaw 36495 diclspsn 39208 areaquad 41047 sprsymrelf 44947 |
Copyright terms: Public domain | W3C validator |