Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elopab | Structured version Visualization version GIF version |
Description: Membership in a class abstraction of pairs. (Contributed by NM, 24-Mar-1998.) |
Ref | Expression |
---|---|
elopab | ⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3510 | . 2 ⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} → 𝐴 ∈ V) | |
2 | opex 5347 | . . . . 5 ⊢ 〈𝑥, 𝑦〉 ∈ V | |
3 | eleq1 2897 | . . . . 5 ⊢ (𝐴 = 〈𝑥, 𝑦〉 → (𝐴 ∈ V ↔ 〈𝑥, 𝑦〉 ∈ V)) | |
4 | 2, 3 | mpbiri 259 | . . . 4 ⊢ (𝐴 = 〈𝑥, 𝑦〉 → 𝐴 ∈ V) |
5 | 4 | adantr 481 | . . 3 ⊢ ((𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑) → 𝐴 ∈ V) |
6 | 5 | exlimivv 1924 | . 2 ⊢ (∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑) → 𝐴 ∈ V) |
7 | eqeq1 2822 | . . . . 5 ⊢ (𝑧 = 𝐴 → (𝑧 = 〈𝑥, 𝑦〉 ↔ 𝐴 = 〈𝑥, 𝑦〉)) | |
8 | 7 | anbi1d 629 | . . . 4 ⊢ (𝑧 = 𝐴 → ((𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ (𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
9 | 8 | 2exbidv 1916 | . . 3 ⊢ (𝑧 = 𝐴 → (∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
10 | df-opab 5120 | . . 3 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} | |
11 | 9, 10 | elab2g 3665 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
12 | 1, 6, 11 | pm5.21nii 380 | 1 ⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 = wceq 1528 ∃wex 1771 ∈ wcel 2105 Vcvv 3492 〈cop 4563 {copab 5119 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pr 5320 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-opab 5120 |
This theorem is referenced by: rexopabb 5406 opelopabsbALT 5407 opelopabsb 5408 opelopabt 5410 opelopabga 5411 opabn0 5431 iunopab 5437 elopabr 5438 0nelopab 5443 epelgOLD 5460 elxp 5571 elopaelxp 5634 elopaba 5674 elcnv 5740 dfmpt3 6475 fmptsng 6922 fmptsnd 6923 opabex3d 7655 opabex3rd 7656 opabex3 7657 fsplit 7801 fsplitOLD 7802 rtrclreclem3 14407 isfunc 17122 griedg0ssusgr 26974 rgrusgrprc 27298 brabgaf 30287 qqhval2 31122 eulerpartlemgvv 31533 satfvsucsuc 32509 satf0op 32521 opelopabd 34325 opelopabb 34326 poimirlem26 34799 ecxrn 35519 dicelval3 38196 pellexlem5 39308 pellex 39310 opelopab4 40762 sprsymrelfvlem 43529 uspgrsprf 43898 uspgrsprf1 43899 |
Copyright terms: Public domain | W3C validator |