Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > inopab | Structured version Visualization version GIF version |
Description: Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.) |
Ref | Expression |
---|---|
inopab | ⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relopab 5690 | . . 3 ⊢ Rel {〈𝑥, 𝑦〉 ∣ 𝜑} | |
2 | relin1 5679 | . . 3 ⊢ (Rel {〈𝑥, 𝑦〉 ∣ 𝜑} → Rel ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓})) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ Rel ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓}) |
4 | relopab 5690 | . 2 ⊢ Rel {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)} | |
5 | sban 2082 | . . . 4 ⊢ ([𝑤 / 𝑦]([𝑧 / 𝑥]𝜑 ∧ [𝑧 / 𝑥]𝜓) ↔ ([𝑤 / 𝑦][𝑧 / 𝑥]𝜑 ∧ [𝑤 / 𝑦][𝑧 / 𝑥]𝜓)) | |
6 | sban 2082 | . . . . 5 ⊢ ([𝑧 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑧 / 𝑥]𝜑 ∧ [𝑧 / 𝑥]𝜓)) | |
7 | 6 | sbbii 2077 | . . . 4 ⊢ ([𝑤 / 𝑦][𝑧 / 𝑥](𝜑 ∧ 𝜓) ↔ [𝑤 / 𝑦]([𝑧 / 𝑥]𝜑 ∧ [𝑧 / 𝑥]𝜓)) |
8 | opelopabsbALT 5408 | . . . . 5 ⊢ (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑) | |
9 | opelopabsbALT 5408 | . . . . 5 ⊢ (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜓) | |
10 | 8, 9 | anbi12i 628 | . . . 4 ⊢ ((〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ∧ 〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜓}) ↔ ([𝑤 / 𝑦][𝑧 / 𝑥]𝜑 ∧ [𝑤 / 𝑦][𝑧 / 𝑥]𝜓)) |
11 | 5, 7, 10 | 3bitr4ri 306 | . . 3 ⊢ ((〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ∧ 〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜓}) ↔ [𝑤 / 𝑦][𝑧 / 𝑥](𝜑 ∧ 𝜓)) |
12 | elin 4168 | . . 3 ⊢ (〈𝑧, 𝑤〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓}) ↔ (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ∧ 〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜓})) | |
13 | opelopabsbALT 5408 | . . 3 ⊢ (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)} ↔ [𝑤 / 𝑦][𝑧 / 𝑥](𝜑 ∧ 𝜓)) | |
14 | 11, 12, 13 | 3bitr4i 305 | . 2 ⊢ (〈𝑧, 𝑤〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓}) ↔ 〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)}) |
15 | 3, 4, 14 | eqrelriiv 5657 | 1 ⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)} |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 398 = wceq 1533 [wsb 2065 ∈ wcel 2110 ∩ cin 3934 〈cop 4566 {copab 5120 Rel wrel 5554 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3496 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-sn 4561 df-pr 4563 df-op 4567 df-opab 5121 df-xp 5555 df-rel 5556 |
This theorem is referenced by: inxp 5697 resopab 5896 fndmin 6809 cnvoprab 7752 epinid0 9058 cnvepnep 9065 wemapwe 9154 dfiso2 17036 frgpuplem 18892 ltbwe 20247 opsrtoslem1 20258 pjfval2 20847 lgsquadlem3 25952 br1cosscnvxrn 35708 1cosscnvxrn 35709 dnwech 39641 fgraphopab 39803 |
Copyright terms: Public domain | W3C validator |