![]() |
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 5480 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 5419 | . 2 ⊢ 〈𝑥, 𝑦〉 ∈ V | |
2 | copsexgw 5445 | . . 3 ⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑))) | |
3 | 2 | bicomd 222 | . 2 ⊢ (𝑧 = 〈𝑥, 𝑦〉 → (∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜑)) |
4 | df-opab 5166 | . 2 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} | |
5 | 1, 3, 4 | elab2 3632 | 1 ⊢ (〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 = wceq 1541 ∃wex 1781 ∈ wcel 2106 〈cop 4590 {copab 5165 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-12 2171 ax-ext 2707 ax-sep 5254 ax-nul 5261 ax-pr 5382 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-opab 5166 |
This theorem is referenced by: rexopabb 5483 ssopab2bw 5502 dmopab 5869 rnopab 5907 funopab 6533 opabiota 6921 fvopab5 6977 f1ompt 7055 ovid 7492 zfrep6 7883 enssdom 8913 omxpenlem 9013 infxpenlem 9945 canthwelem 10582 pospo 18226 2ndcdisj 22791 lgsquadlem1 26712 lgsquadlem2 26713 h2hlm 29808 opabdm 31416 opabrn 31417 fpwrelmap 31533 eulerpartlemgvv 32845 fineqvrep 33565 satfvsucsuc 33828 bj-opelopabid 35625 phpreu 36029 poimirlem26 36071 vvdifopab 36687 brabidgaw 36793 diclspsn 39624 areaquad 41488 sprsymrelf 45619 |
Copyright terms: Public domain | W3C validator |