![]() |
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 5687 available. Check if it is shorter to prove bj-epelg 35470 first or bj-epelb 35471 first. (Contributed by BJ, 14-Jul-2023.) |
Ref | Expression |
---|---|
bj-epelb | ⊢ (𝐴 E 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rele 5781 | . . . 4 ⊢ Rel E | |
2 | 1 | brrelex2i 5687 | . . 3 ⊢ (𝐴 E 𝐵 → 𝐵 ∈ V) |
3 | 2 | pm4.71i 560 | . 2 ⊢ (𝐴 E 𝐵 ↔ (𝐴 E 𝐵 ∧ 𝐵 ∈ V)) |
4 | epelg 5536 | . . 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 2106 Vcvv 3443 class class class wbr 5103 E cep 5534 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2708 ax-sep 5254 ax-nul 5261 ax-pr 5382 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-br 5104 df-opab 5166 df-eprel 5535 df-xp 5637 df-rel 5638 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |