| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > relopabiv | Structured version Visualization version GIF version | ||
| Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but a longer proof using ax-11 2157 and ax-12 2177, see relopabi 5832. (Contributed by BJ, 22-Jul-2023.) |
| Ref | Expression |
|---|---|
| relopabiv.1 | ⊢ 𝐴 = {〈𝑥, 𝑦〉 ∣ 𝜑} |
| Ref | Expression |
|---|---|
| relopabiv | ⊢ Rel 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex 3484 | . . . . . 6 ⊢ 𝑥 ∈ V | |
| 2 | vex 3484 | . . . . . 6 ⊢ 𝑦 ∈ V | |
| 3 | 1, 2 | pm3.2i 470 | . . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V) |
| 4 | 3 | a1i 11 | . . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V)) |
| 5 | 4 | ssopab2i 5555 | . . 3 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} |
| 6 | relopabiv.1 | . . 3 ⊢ 𝐴 = {〈𝑥, 𝑦〉 ∣ 𝜑} | |
| 7 | df-xp 5691 | . . 3 ⊢ (V × V) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} | |
| 8 | 5, 6, 7 | 3sstr4i 4035 | . 2 ⊢ 𝐴 ⊆ (V × V) |
| 9 | df-rel 5692 | . 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) | |
| 10 | 8, 9 | mpbir 231 | 1 ⊢ Rel 𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 395 = wceq 1540 ∈ wcel 2108 Vcvv 3480 ⊆ wss 3951 {copab 5205 × cxp 5683 Rel wrel 5690 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-opab 5206 df-xp 5691 df-rel 5692 |
| This theorem is referenced by: relopabv 5831 mptrel 5835 reli 5836 rele 5837 relcnv 6122 relco 6126 brfvopabrbr 7013 reloprab 7492 reldmoprab 7540 relrpss 7744 eqer 8781 ecopover 8861 relen 8990 reldom 8991 relfsupp 9403 relwdom 9606 fpwwe2lem2 10672 fpwwe2lem3 10673 fpwwe2lem5 10675 fpwwe2lem6 10676 fpwwe2lem8 10678 fpwwe2lem10 10680 fpwwe2lem11 10681 fpwwe2lem12 10682 fpwwelem 10685 climrel 15528 rlimrel 15529 brstruct 17185 sscrel 17857 gaorber 19326 sylow2a 19637 efgrelexlemb 19768 efgcpbllemb 19773 rellindf 21828 psrbaglesupp 21942 2ndcctbss 23463 refrel 23516 vitalilem1 25643 lgsquadlem1 27424 lgsquadlem2 27425 dmscut 27856 relsubgr 29286 vcrel 30579 h2hlm 30999 hlimi 31207 erler 33269 relfldext 33697 relmntop 34025 relae 34241 fnerel 36339 filnetlem3 36381 brabg2 37724 heiborlem3 37820 heiborlem4 37821 relrngo 37903 isdivrngo 37957 drngoi 37958 isdrngo1 37963 riscer 37995 relcoss 38424 relssr 38501 prter1 38880 prter3 38883 prjsper 42618 reldvds 44334 nelbrim 47287 rellininds 48360 |
| Copyright terms: Public domain | W3C validator |