Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-epelb | Structured version Visualization version GIF version |
Description: Two classes are related by the membership relation if and only if they are related by the membership relation (i.e., the first is an element of the second) and the second is a set (hence so is the first). TODO: move to Main after reordering to have brrelex2i 5675 available. Check if it is shorter to prove bj-epelg 35352 first or bj-epelb 35353 first. (Contributed by BJ, 14-Jul-2023.) |
Ref | Expression |
---|---|
bj-epelb | ⊢ (𝐴 E 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rele 5769 | . . . 4 ⊢ Rel E | |
2 | 1 | brrelex2i 5675 | . . 3 ⊢ (𝐴 E 𝐵 → 𝐵 ∈ V) |
3 | 2 | pm4.71i 560 | . 2 ⊢ (𝐴 E 𝐵 ↔ (𝐴 E 𝐵 ∧ 𝐵 ∈ V)) |
4 | epelg 5525 | . . 3 ⊢ (𝐵 ∈ V → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
5 | 4 | pm5.32ri 576 | . 2 ⊢ ((𝐴 E 𝐵 ∧ 𝐵 ∈ V) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V)) |
6 | 3, 5 | bitri 274 | 1 ⊢ (𝐴 E 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 ∈ wcel 2105 Vcvv 3441 class class class wbr 5092 E cep 5523 |
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 2707 ax-sep 5243 ax-nul 5250 ax-pr 5372 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2714 df-cleq 2728 df-clel 2814 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3404 df-v 3443 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4270 df-if 4474 df-sn 4574 df-pr 4576 df-op 4580 df-br 5093 df-opab 5155 df-eprel 5524 df-xp 5626 df-rel 5627 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |