brrelex2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > brrelex2		Structured version Visualization version GIF version

Theorem brrelex2 5734

Description: If two classes are related by a binary relation, then the second class is a set. (Contributed by Mario Carneiro, 26-Apr-2015.)

**Assertion**
Ref	Expression
brrelex2	⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)

**Proof of Theorem brrelex2**
Step	Hyp	Ref	Expression
1		brrelex12 5732	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2	1	simprd 494	1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2098 Vcvv 3471 class class class wbr 5150 Rel wrel 5685

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2698 ax-sep 5301 ax-nul 5308 ax-pr 5431

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2705 df-cleq 2719 df-clel 2805 df-ral 3058 df-rex 3067 df-rab 3429 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4325 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5151 df-opab 5213 df-xp 5686 df-rel 5687

This theorem is referenced by: brrelex2i 5737 releldm 5948 relelrn 5949 elrelimasn 6092 funbrfv 6951 relbrtpos 8247 ertr 8744 erth 8779 fsuppss 9412 pslem 18569 opeldifid 32407 eqvreltr 38083 eqvrelth 38087 frege124d 43194 frege133d 43198 climfv 45081 funbrafv2 46629

	
		OSZAR »