P. 361 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36001-36100   *Has distinct variable group(s)

Type	Label	Description
Statement
21.11.13  Hypothesis builders
Theorem	hbntg 36001	A more general form of hbnt 2301. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) → (¬ 𝜓 → ∀𝑥 ¬ 𝜑))
Theorem	hbimtg 36002	A more general and closed form of hbim 2306. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ((∀𝑥(𝜑 → ∀𝑥𝜒) ∧ (𝜓 → ∀𝑥𝜃)) → ((𝜒 → 𝜓) → ∀𝑥(𝜑 → 𝜃)))
Theorem	hbaltg 36003	A more general and closed form of hbal 2173. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜓) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜓))
Theorem	hbng 36004	A more general form of hbn 2302. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (𝜑 → ∀𝑥𝜓)    ⇒   ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜑)
Theorem	hbimg 36005	A more general form of hbim 2306. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜒 → ∀𝑥𝜃)    ⇒   ⊢ ((𝜓 → 𝜒) → ∀𝑥(𝜑 → 𝜃))
21.11.14  Well-founded zero, successor, and limits
Syntax	cwsuc 36006	Declare the syntax for well-founded successor.
class wsuc(𝑅, 𝐴, 𝑋)
Syntax	cwlim 36007	Declare the syntax for well-founded limit class.
class WLim(𝑅, 𝐴)
Definition	df-wsuc 36008	Define the concept of a successor in a well-founded set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.)
⊢ wsuc(𝑅, 𝐴, 𝑋) = inf(Pred(◡𝑅, 𝐴, 𝑋), 𝐴, 𝑅)
Definition	df-wlim 36009*	Define the class of limit points of a well-founded set. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.)
⊢ WLim(𝑅, 𝐴) = {𝑥 ∈ 𝐴 ∣ (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))}
Theorem	wsuceq123 36010	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌) → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑆, 𝐵, 𝑌))
Theorem	wsuceq1 36011	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑅 = 𝑆 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑆, 𝐴, 𝑋))
Theorem	wsuceq2 36012	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝐴 = 𝐵 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑅, 𝐵, 𝑋))
Theorem	wsuceq3 36013	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑋 = 𝑌 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑅, 𝐴, 𝑌))
Theorem	nfwsuc 36014	Bound-variable hypothesis builder for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝑋    ⇒   ⊢ Ⅎ𝑥wsuc(𝑅, 𝐴, 𝑋)
Theorem	wlimeq12 36015	Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → WLim(𝑅, 𝐴) = WLim(𝑆, 𝐵))
Theorem	wlimeq1 36016	Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.)
⊢ (𝑅 = 𝑆 → WLim(𝑅, 𝐴) = WLim(𝑆, 𝐴))
Theorem	wlimeq2 36017	Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.)
⊢ (𝐴 = 𝐵 → WLim(𝑅, 𝐴) = WLim(𝑅, 𝐵))
Theorem	nfwlim 36018	Bound-variable hypothesis builder for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥WLim(𝑅, 𝐴)
Theorem	elwlim 36019	Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.)
⊢ (𝑋 ∈ WLim(𝑅, 𝐴) ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑋 = sup(Pred(𝑅, 𝐴, 𝑋), 𝐴, 𝑅)))
Theorem	wzel 36020	The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.)
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) → inf(𝐴, 𝐴, 𝑅) ∈ 𝐴)
Theorem	wsuclem 36021*	Lemma for the supremum properties of well-founded successor. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.)
⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ∃𝑤 ∈ 𝐴 𝑋𝑅𝑤)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ Pred (◡𝑅, 𝐴, 𝑋) ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑧𝑅𝑦)))
Theorem	wsucex 36022	Existence theorem for well-founded successor. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → wsuc(𝑅, 𝐴, 𝑋) ∈ V)
Theorem	wsuccl 36023*	If 𝑋 is a set with an 𝑅 successor in 𝐴, then its well-founded successor is a member of 𝐴. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝑋𝑅𝑦)    ⇒   ⊢ (𝜑 → wsuc(𝑅, 𝐴, 𝑋) ∈ 𝐴)
Theorem	wsuclb 36024	A well-founded successor is a lower bound on points after 𝑋. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋𝑅𝑌)    ⇒   ⊢ (𝜑 → ¬ 𝑌𝑅wsuc(𝑅, 𝐴, 𝑋))
Theorem	wlimss 36025	The class of limit points is a subclass of the base class. (Contributed by Scott Fenton, 16-Jun-2018.)
⊢ WLim(𝑅, 𝐴) ⊆ 𝐴
21.11.15  Quantifier-free definitions
Syntax	ctxp 36026	Declare the syntax for tail Cartesian product.
class (𝐴 ⊗ 𝐵)
Syntax	cpprod 36027	Declare the syntax for the parallel product.
class pprod(𝑅, 𝑆)
Syntax	csset 36028	Declare the subset relationship class.
class SSet
Syntax	ctrans 36029	Declare the transitive set class.
class Trans
Syntax	cbigcup 36030	Declare the set union relationship.
class Bigcup
Syntax	cfix 36031	Declare the syntax for the fixpoints of a class.
class Fix 𝐴
Syntax	climits 36032	Declare the class of limit ordinals.
class Limits
Syntax	cfuns 36033	Declare the syntax for the class of all function.
class Funs
Syntax	csingle 36034	Declare the syntax for the singleton function.
class Singleton
Syntax	csingles 36035	Declare the syntax for the class of all singletons.
class Singletons
Syntax	cimage 36036	Declare the syntax for the image functor.
class Image𝐴
Syntax	ccart 36037	Declare the syntax for the cartesian function.
class Cart
Syntax	cimg 36038	Declare the syntax for the image function.
class Img
Syntax	cdomain 36039	Declare the syntax for the domain function.
class Domain
Syntax	crange 36040	Declare the syntax for the range function.
class Range
Syntax	capply 36041	Declare the syntax for the application function.
class Apply
Syntax	ccup 36042	Declare the syntax for the cup function.
class Cup
Syntax	ccap 36043	Declare the syntax for the cap function.
class Cap
Syntax	csuccf 36044	Declare the syntax for the successor function.
class Succ
Syntax	cfunpart 36045	Declare the syntax for the functional part functor.
class Funpart𝐹
Syntax	cfullfn 36046	Declare the syntax for the full function functor.
class FullFun𝐹
Syntax	crestrict 36047	Declare the syntax for the restriction function.
class Restrict
Syntax	cub 36048	Declare the syntax for the upper bound relationship functor.
class UB𝑅
Syntax	clb 36049	Declare the syntax for the lower bound relationship functor.
class LB𝑅
Definition	df-txp 36050	Define the tail cross of two classes. Membership in this class is defined by txpss3v 36074 and brtxp 36076. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ⊗ 𝐵) = ((◡(1st ↾ (V × V)) ∘ 𝐴) ∩ (◡(2nd ↾ (V × V)) ∘ 𝐵))
Definition	df-pprod 36051	Define the parallel product of two classes. Membership in this class is defined by pprodss4v 36080 and brpprod 36081. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ pprod(𝐴, 𝐵) = ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V))))
Definition	df-sset 36052	Define the subset class. For the value, see brsset 36085. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ SSet = ((V × V) ∖ ran ( E ⊗ (V ∖ E )))
Definition	df-trans 36053	Define the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Trans = (V ∖ ran (( E ∘ E ) ∖ E ))
Definition	df-bigcup 36054	Define the Bigcup function, which, per fvbigcup 36098, carries a set to its union. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Bigcup = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ E ) ⊗ V)))
Definition	df-fix 36055	Define the class of all fixpoints of a relationship. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Fix 𝐴 = dom (𝐴 ∩ I )
Definition	df-limits 36056	Define the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Limits = ((On ∩ Fix Bigcup ) ∖ {∅})
Definition	df-funs 36057	Define the class of all functions. See elfuns 36111 for membership. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )))
Definition	df-singleton 36058	Define the singleton function. See brsingle 36113 for its value. (Contributed by Scott Fenton, 4-Apr-2014.)
⊢ Singleton = ((V × V) ∖ ran ((V ⊗ E ) △ ( I ⊗ V)))
Definition	df-singles 36059	Define the class of all singletons. See elsingles 36114 for membership. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ Singletons = ran Singleton
Definition	df-image 36060	Define the image functor. This function takes a set 𝐴 to a function 𝑥 ↦ (𝐴 “ 𝑥), providing that the latter exists. See imageval 36126 for the derivation. (Contributed by Scott Fenton, 27-Mar-2014.)
⊢ Image𝐴 = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ ◡𝐴) ⊗ V)))
Definition	df-cart 36061	Define the cartesian product function. See brcart 36128 for its value. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ Cart = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (pprod( E , E ) ⊗ V)))
Definition	df-img 36062	Define the image function. See brimg 36133 for its value. (Contributed by Scott Fenton, 12-Apr-2014.)
⊢ Img = (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart)
Definition	df-domain 36063	Define the domain function. See brdomain 36129 for its value. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ Domain = Image(1st ↾ (V × V))
Definition	df-range 36064	Define the range function. See brrange 36130 for its value. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ Range = Image(2nd ↾ (V × V))
Definition	df-cup 36065	Define the little cup function. See brcup 36135 for its value. (Contributed by Scott Fenton, 14-Apr-2014.)
⊢ Cup = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (((◡1st ∘ E ) ∪ (◡2nd ∘ E )) ⊗ V)))
Definition	df-cap 36066	Define the little cap function. See brcap 36136 for its value. (Contributed by Scott Fenton, 17-Apr-2014.)
⊢ Cap = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (((◡1st ∘ E ) ∩ (◡2nd ∘ E )) ⊗ V)))
Definition	df-restrict 36067	Define the restriction function. See brrestrict 36147 for its value. (Contributed by Scott Fenton, 17-Apr-2014.)
⊢ Restrict = (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))
Definition	df-succf 36068	Define the successor function. See its alternate version dfsuccf2 36139. See brsuccf 36138 for its value. Cf. the equivalent df-sucmap 38797 family. (Contributed by Scott Fenton, 14-Apr-2014.)
⊢ Succ = (Cup ∘ ( I ⊗ Singleton))
Definition	df-apply 36069	Define the application function. See brapply 36134 for its value. (Contributed by Scott Fenton, 12-Apr-2014.)
⊢ Apply = (( Bigcup ∘ Bigcup ) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton))))
Definition	df-funpart 36070	Define the functional part of a class 𝐹. This is the maximal part of 𝐹 that is a function. See funpartfun 36141 and funpartfv 36143 for the meaning of this statement. (Contributed by Scott Fenton, 16-Apr-2014.)
⊢ Funpart𝐹 = (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))
Definition	df-fullfun 36071	Define the full function over 𝐹. This is a function with domain V that always agrees with 𝐹 for its value. (Contributed by Scott Fenton, 17-Apr-2014.)
⊢ FullFun𝐹 = (Funpart𝐹 ∪ ((V ∖ dom Funpart𝐹) × {∅}))
Definition	df-ub 36072	Define the upper bound relationship functor. See brub 36152 for value. (Contributed by Scott Fenton, 3-May-2018.)
⊢ UB𝑅 = ((V × V) ∖ ((V ∖ 𝑅) ∘ ◡ E ))
Definition	df-lb 36073	Define the lower bound relationship functor. See brlb 36153 for value. (Contributed by Scott Fenton, 3-May-2018.)
⊢ LB𝑅 = UB◡𝑅
Theorem	txpss3v 36074	A tail Cartesian product is a subset of the class of ordered triples. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ⊗ 𝐵) ⊆ (V × (V × V))
Theorem	txprel 36075	A tail Cartesian product is a relationship. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Rel (𝐴 ⊗ 𝐵)
Theorem	brtxp 36076	Characterize a ternary relation over a tail Cartesian product. Together with txpss3v 36074, this completely defines membership in a tail cross. (Contributed by Scott Fenton, 31-Mar-2012.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ (𝑋(𝐴 ⊗ 𝐵)⟨𝑌, 𝑍⟩ ↔ (𝑋𝐴𝑌 ∧ 𝑋𝐵𝑍))
Theorem	brtxp2 36077*	The binary relation over a tail cross when the second argument is not an ordered pair. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 3-May-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴(𝑅 ⊗ 𝑆)𝐵 ↔ ∃𝑥∃𝑦(𝐵 = ⟨𝑥, 𝑦⟩ ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦))
Theorem	dfpprod2 36078	Expanded definition of parallel product. (Contributed by Scott Fenton, 3-May-2014.)
⊢ pprod(𝐴, 𝐵) = ((◡(1st ↾ (V × V)) ∘ (𝐴 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐵 ∘ (2nd ↾ (V × V)))))
Theorem	pprodcnveq 36079	A converse law for parallel product. (Contributed by Scott Fenton, 3-May-2014.)
⊢ pprod(𝑅, 𝑆) = ◡pprod(◡𝑅, ◡𝑆)
Theorem	pprodss4v 36080	The parallel product is a subclass of ((V × V) × (V × V)). (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ pprod(𝐴, 𝐵) ⊆ ((V × V) × (V × V))
Theorem	brpprod 36081	Characterize a quaternary relation over a tail Cartesian product. Together with pprodss4v 36080, this completely defines membership in a parallel product. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑍 ∈ V    &   ⊢ 𝑊 ∈ V    ⇒   ⊢ (⟨𝑋, 𝑌⟩pprod(𝐴, 𝐵)⟨𝑍, 𝑊⟩ ↔ (𝑋𝐴𝑍 ∧ 𝑌𝐵𝑊))
Theorem	brpprod3a 36082*	Condition for parallel product when the last argument is not an ordered pair. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ (⟨𝑋, 𝑌⟩pprod(𝑅, 𝑆)𝑍 ↔ ∃𝑧∃𝑤(𝑍 = ⟨𝑧, 𝑤⟩ ∧ 𝑋𝑅𝑧 ∧ 𝑌𝑆𝑤))
Theorem	brpprod3b 36083*	Condition for parallel product when the first argument is not an ordered pair. (Contributed by Scott Fenton, 3-May-2014.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ (𝑋pprod(𝑅, 𝑆)⟨𝑌, 𝑍⟩ ↔ ∃𝑧∃𝑤(𝑋 = ⟨𝑧, 𝑤⟩ ∧ 𝑧𝑅𝑌 ∧ 𝑤𝑆𝑍))
Theorem	relsset 36084	The subset class is a binary relation. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Rel SSet
Theorem	brsset 36085	For sets, the SSet binary relation is equivalent to the subset relationship. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 SSet 𝐵 ↔ 𝐴 ⊆ 𝐵)
Theorem	idsset 36086	I is equal to the intersection of SSet and its converse. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ I = ( SSet ∩ ◡ SSet )
Theorem	eltrans 36087	Membership in the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Trans ↔ Tr 𝐴)
Theorem	dfon3 36088	A quantifier-free definition of On. (Contributed by Scott Fenton, 5-Apr-2012.)
⊢ On = (V ∖ ran (( SSet ∩ ( Trans × V)) ∖ ( I ∪ E )))
Theorem	dfon4 36089	Another quantifier-free definition of On. (Contributed by Scott Fenton, 4-May-2014.)
⊢ On = (V ∖ (( SSet ∖ ( I ∪ E )) “ Trans ))
Theorem	brtxpsd 36090*	Expansion of a common form used in quantifier-free definitions. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (¬ 𝐴ran ((V ⊗ E ) △ (𝑅 ⊗ V))𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥𝑅𝐴))
Theorem	brtxpsd2 36091*	Another common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 21-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑅 = (𝐶 ∖ ran ((V ⊗ E ) △ (𝑆 ⊗ V)))    &   ⊢ 𝐴𝐶𝐵    ⇒   ⊢ (𝐴𝑅𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥𝑆𝐴))
Theorem	brtxpsd3 36092*	A third common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 3-May-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑅 = (𝐶 ∖ ran ((V ⊗ E ) △ (𝑆 ⊗ V)))    &   ⊢ 𝐴𝐶𝐵    &   ⊢ (𝑥 ∈ 𝑋 ↔ 𝑥𝑆𝐴)    ⇒   ⊢ (𝐴𝑅𝐵 ↔ 𝐵 = 𝑋)
Theorem	relbigcup 36093	The Bigcup relationship is a relationship. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Rel Bigcup
Theorem	brbigcup 36094	Binary relation over Bigcup . (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 Bigcup 𝐵 ↔ ∪ 𝐴 = 𝐵)
Theorem	dfbigcup2 36095	Bigcup using maps-to notation. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Bigcup = (𝑥 ∈ V ↦ ∪ 𝑥)
Theorem	fobigcup 36096	Bigcup maps the universe onto itself. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Bigcup :V–onto→V
Theorem	fnbigcup 36097	Bigcup is a function over the universal class. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Bigcup Fn V
Theorem	fvbigcup 36098	For sets, Bigcup yields union. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ( Bigcup ‘𝐴) = ∪ 𝐴
Theorem	elfix 36099	Membership in the fixpoints of a class. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Fix 𝑅 ↔ 𝐴𝑅𝐴)
Theorem	elfix2 36100	Alternative membership in the fixpoint of a class. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Rel 𝑅    ⇒   ⊢ (𝐴 ∈ Fix 𝑅 ↔ 𝐴𝑅𝐴)