Theorem bj-epelb 35219

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 5643 available. Check if it is shorter to prove bj-epelg 35218 first or bj-epelb 35219 first. (Contributed by BJ, 14-Jul-2023.)

Assertion

Ref	Expression
bj-epelb	⊢ (𝐴 E 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V))

Proof of Theorem bj-epelb

Step	Hyp	Ref	Expression
1		rele 5734	. . . 4 ⊢ Rel E
2	1	brrelex2i 5643	. . 3 ⊢ (𝐴 E 𝐵 → 𝐵 ∈ V)
3	2	pm4.71i 559	. 2 ⊢ (𝐴 E 𝐵 ↔ (𝐴 E 𝐵 ∧ 𝐵 ∈ V))
4		epelg 5495	. . 3 ⊢ (𝐵 ∈ V → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵))
5	4	pm5.32ri 575	. 2 ⊢ ((𝐴 E 𝐵 ∧ 𝐵 ∈ V) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V))
6	3, 5	bitri 274	1 ⊢ (𝐴 E 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V))

Syntax hints:   ↔ wb 205   ∧ wa 395   ∈ wcel 2109  Vcvv 3430   class class class wbr 5078   E cep 5493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-opab 5141  df-eprel 5494  df-xp 5594  df-rel 5595

This theorem is referenced by: (None)