![]() |
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 3243 | . 2 ⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} → 𝐴 ∈ V) | |
2 | opex 4962 | . . . . 5 ⊢ 〈𝑥, 𝑦〉 ∈ V | |
3 | eleq1 2718 | . . . . 5 ⊢ (𝐴 = 〈𝑥, 𝑦〉 → (𝐴 ∈ V ↔ 〈𝑥, 𝑦〉 ∈ V)) | |
4 | 2, 3 | mpbiri 248 | . . . 4 ⊢ (𝐴 = 〈𝑥, 𝑦〉 → 𝐴 ∈ V) |
5 | 4 | adantr 480 | . . 3 ⊢ ((𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑) → 𝐴 ∈ V) |
6 | 5 | exlimivv 1900 | . 2 ⊢ (∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑) → 𝐴 ∈ V) |
7 | eqeq1 2655 | . . . . 5 ⊢ (𝑧 = 𝐴 → (𝑧 = 〈𝑥, 𝑦〉 ↔ 𝐴 = 〈𝑥, 𝑦〉)) | |
8 | 7 | anbi1d 741 | . . . 4 ⊢ (𝑧 = 𝐴 → ((𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ (𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
9 | 8 | 2exbidv 1892 | . . 3 ⊢ (𝑧 = 𝐴 → (∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
10 | df-opab 4746 | . . 3 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} | |
11 | 9, 10 | elab2g 3385 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
12 | 1, 6, 11 | pm5.21nii 367 | 1 ⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 = wceq 1523 ∃wex 1744 ∈ wcel 2030 Vcvv 3231 〈cop 4216 {copab 4745 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-nul 4822 ax-pr 4936 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-opab 4746 |
This theorem is referenced by: opelopabsbALT 5013 opelopabsb 5014 opelopabt 5016 opelopabga 5017 opabn0 5035 iunopab 5041 elopabr 5042 epelg 5059 elxp 5165 elopaelxp 5225 elopaba 5265 elcnv 5331 dfmpt3 6052 fmptsng 6475 fmptsnd 6476 0neqopab 6740 opabex3d 7187 opabex3 7188 fsplit 7327 rtrclreclem3 13844 isfunc 16571 griedg0ssusgr 26202 rgrusgrprc 26541 brabgaf 29546 qqhval2 30154 eulerpartlemgvv 30566 poimirlem26 33565 ecxrn 34289 dicelval3 36786 pellexlem5 37714 pellex 37716 opelopab4 39084 sprsymrelfvlem 42065 uspgrsprf 42079 uspgrsprf1 42080 |
Copyright terms: Public domain | W3C validator |