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 3451 | . 2 ⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} → 𝐴 ∈ V) | |
2 | opex 5380 | . . . . 5 ⊢ 〈𝑥, 𝑦〉 ∈ V | |
3 | eleq1 2827 | . . . . 5 ⊢ (𝐴 = 〈𝑥, 𝑦〉 → (𝐴 ∈ V ↔ 〈𝑥, 𝑦〉 ∈ V)) | |
4 | 2, 3 | mpbiri 257 | . . . 4 ⊢ (𝐴 = 〈𝑥, 𝑦〉 → 𝐴 ∈ V) |
5 | 4 | adantr 481 | . . 3 ⊢ ((𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑) → 𝐴 ∈ V) |
6 | 5 | exlimivv 1936 | . 2 ⊢ (∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑) → 𝐴 ∈ V) |
7 | elopabw 5440 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑))) | |
8 | 1, 6, 7 | pm5.21nii 380 | 1 ⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 = wceq 1539 ∃wex 1782 ∈ wcel 2107 Vcvv 3433 〈cop 4568 {copab 5137 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2710 ax-sep 5224 ax-nul 5231 ax-pr 5353 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2069 df-clab 2717 df-cleq 2731 df-clel 2817 df-v 3435 df-dif 3891 df-un 3893 df-nul 4258 df-if 4461 df-sn 4563 df-pr 4565 df-op 4569 df-opab 5138 |
This theorem is referenced by: rexopabb 5442 vopelopabsb 5443 opelopabsb 5444 opelopabt 5446 opelopabga 5447 opabn0 5467 iunopabOLD 5474 elopabrOLD 5477 0nelopab 5481 0nelopabOLD 5482 elxp 5613 elopaelxpOLD 5678 elopaba 5720 elcnv 5788 dfmpt3 6576 fmptsng 7049 fmptsnd 7050 opabex3d 7817 opabex3rd 7818 opabex3 7819 fsplit 7966 fsplitOLD 7967 rtrclreclem3 14780 isfunc 17588 griedg0ssusgr 27641 rgrusgrprc 27965 brabgaf 30957 qqhval2 31941 eulerpartlemgvv 32352 satfvsucsuc 33336 satf0op 33348 opelopabd 35321 opelopabb 35322 poimirlem26 35812 ecxrn 36524 dicelval3 39201 pellexlem5 40662 pellex 40664 opelopab4 42178 sprsymrelfvlem 44953 uspgrsprf 45319 uspgrsprf1 45320 |
Copyright terms: Public domain | W3C validator |