![]() |
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 ordered pairs. (Contributed by NM, 24-Mar-1998.) |
Ref | Expression |
---|---|
elopab | ⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3492 | . 2 ⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} → 𝐴 ∈ V) | |
2 | opex 5464 | . . . . 5 ⊢ 〈𝑥, 𝑦〉 ∈ V | |
3 | eleq1 2820 | . . . . 5 ⊢ (𝐴 = 〈𝑥, 𝑦〉 → (𝐴 ∈ V ↔ 〈𝑥, 𝑦〉 ∈ V)) | |
4 | 2, 3 | mpbiri 258 | . . . 4 ⊢ (𝐴 = 〈𝑥, 𝑦〉 → 𝐴 ∈ V) |
5 | 4 | adantr 480 | . . 3 ⊢ ((𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑) → 𝐴 ∈ V) |
6 | 5 | exlimivv 1934 | . 2 ⊢ (∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑) → 𝐴 ∈ V) |
7 | elopabw 5526 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑))) | |
8 | 1, 6, 7 | pm5.21nii 378 | 1 ⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 395 = wceq 1540 ∃wex 1780 ∈ wcel 2105 Vcvv 3473 〈cop 4634 {copab 5210 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-opab 5211 |
This theorem is referenced by: rexopabb 5528 vopelopabsb 5529 opelopabsb 5530 opelopabt 5532 opelopabga 5533 opabn0 5553 iunopabOLD 5560 elopabrOLD 5563 0nelopab 5567 0nelopabOLD 5568 elxp 5699 elopaelxpOLD 5766 elopaba 5808 elcnv 5876 dfmpt3 6684 fmptsng 7168 fmptsnd 7169 opabex3d 7956 opabex3rd 7957 opabex3 7958 fsplit 8108 rtrclreclem3 15014 isfunc 17821 griedg0ssusgr 28955 rgrusgrprc 29279 brabgaf 32270 qqhval2 33426 eulerpartlemgvv 33839 satfvsucsuc 34820 satf0op 34832 opelopabd 36486 opelopabb 36487 poimirlem26 36978 ecxrn 37721 dicelval3 40515 pellexlem5 42034 pellex 42036 opelopab4 43775 sprsymrelfvlem 46617 uspgrsprf 46983 uspgrsprf1 46984 |
Copyright terms: Public domain | W3C validator |