| Mathbox for Peter Mazsa |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > eldmxrncnvepres | Structured version Visualization version GIF version | ||
| Description: Element of the domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025.) |
| Ref | Expression |
|---|---|
| eldmxrncnvepres | ⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [𝐵]𝑅 ≠ ∅))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eldmres3 38779 | . . 3 ⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ [𝐵]𝑅 ≠ ∅))) | |
| 2 | 1 | anbi1d 640 | . 2 ⊢ (𝐵 ∈ 𝑉 → ((𝐵 ∈ dom (𝑅 ↾ 𝐴) ∧ 𝐵 ≠ ∅) ↔ ((𝐵 ∈ 𝐴 ∧ [𝐵]𝑅 ≠ ∅) ∧ 𝐵 ≠ ∅))) |
| 3 | dmxrncnvepres 38928 | . . . 4 ⊢ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) = (dom (𝑅 ↾ 𝐴) ∖ {∅}) | |
| 4 | 3 | eleq2i 2854 | . . 3 ⊢ (𝐵 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) ↔ 𝐵 ∈ (dom (𝑅 ↾ 𝐴) ∖ {∅})) |
| 5 | eldifsn 4746 | . . 3 ⊢ (𝐵 ∈ (dom (𝑅 ↾ 𝐴) ∖ {∅}) ↔ (𝐵 ∈ dom (𝑅 ↾ 𝐴) ∧ 𝐵 ≠ ∅)) | |
| 6 | 4, 5 | bitri 277 | . 2 ⊢ (𝐵 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) ↔ (𝐵 ∈ dom (𝑅 ↾ 𝐴) ∧ 𝐵 ≠ ∅)) |
| 7 | 3anan32 1108 | . 2 ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [𝐵]𝑅 ≠ ∅) ↔ ((𝐵 ∈ 𝐴 ∧ [𝐵]𝑅 ≠ ∅) ∧ 𝐵 ≠ ∅)) | |
| 8 | 2, 6, 7 | 3bitr4g 316 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [𝐵]𝑅 ≠ ∅))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1098 ∈ wcel 2142 ≠ wne 2957 ∖ cdif 3901 ∅c0 4285 {csn 4582 E cep 5546 ◡ccnv 5646 dom cdm 5647 ↾ cres 5649 [cec 8676 ⋉ cxrn 38670 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-sep 5246 ax-nul 5256 ax-pr 5390 ax-un 7718 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3077 df-rex 3087 df-rab 3415 df-v 3456 df-sbc 3745 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4481 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5542 df-eprel 5547 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-fo 6527 df-fv 6529 df-oprab 7400 df-1st 7970 df-2nd 7971 df-ec 8680 df-xrn 38876 |
| This theorem is referenced by: eceldmqsxrncnvepres 38932 |
| Copyright terms: Public domain | W3C validator |