| 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 5511 with a disjoint variable condition, which does not require ax-13 2406. (Contributed by NM, 14-Apr-1995.) Avoid ax-13 2406. (Revised by GG, 26-Jan-2024.) |
| Ref | Expression |
|---|---|
| opabidw | ⊢ (〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | opex 5447 | . 2 ⊢ 〈𝑥, 𝑦〉 ∈ V | |
| 2 | copsexgw 5474 | . . 3 ⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑))) | |
| 3 | 2 | bicomd 226 | . 2 ⊢ (𝑧 = 〈𝑥, 𝑦〉 → (∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜑)) |
| 4 | df-opab 5176 | . 2 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} | |
| 5 | 1, 3, 4 | elab2 3643 | 1 ⊢ (〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜑) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: ↔ wb 209 ∧ wa 401 = wceq 1570 ∃wex 1812 ∈ wcel 2146 〈cop 4597 {copab 5175 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-pr 5406 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-rab 3419 df-v 3459 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-sn 4592 df-pr 4594 df-op 4598 df-opab 5176 |
| This theorem is used by: rexopabb 5514 ssopab2bw 5534 dmopab 5907 rnopab 5946 funopab 6575 opabiota 6967 fvopab5 7027 f1ompt 7110 ovid 7560 zfrep6OLD 7958 enssdomOLD 8980 omxpenlem 9073 infxpenlem 10013 canthwelem 10652 pospo 18423 2ndcdisj 23666 lgsquadlem1 27597 lgsquadlem2 27598 h2hlm 31405 opabdm 33029 opabrn 33030 fpwrelmap 33150 eulerpartlemgvv 34833 fineqvrep 35586 satfvsucsuc 35896 bj-opelopabid 37890 phpreu 38314 poimirlem26 38356 vvdifopab 38974 brabidgaw 39082 diclspsn 42028 areaquad 44003 sprsymrelf 48304 |
| Copyright terms: Public domain | W3C validator |