P. 411 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41001-41100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ifpim3 41001	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ ((𝜑 → 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜑))
Theorem	ifpnim1 41002	Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜑))
Theorem	ifpim4 41003	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, 𝜓, ¬ 𝜑))
Theorem	ifpnim2 41004	Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜓, ¬ 𝜓, 𝜑))
Theorem	ifpim123g 41005	Implication of conditional logical operators. The right hand side is basically conjunctive normal form which is useful in proofs. (Contributed by RP, 16-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜏) → if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂)))))
Theorem	ifpim1g 41006	Implication of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)) ↔ (((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)) ∧ ((𝜑 → 𝜓) ∨ (𝜒 → 𝜃))))
Theorem	ifp1bi 41007	Substitute the first element of conditional logical operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃)) ↔ ((((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜑 → 𝜓) ∨ (𝜃 → 𝜒))) ∧ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)))))
Theorem	ifpbi1b 41008	When the first variable is irrelevant, it can be replaced. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, 𝜒, 𝜒) ↔ if-(𝜓, 𝜒, 𝜒))
Theorem	ifpimimb 41009	Factor conditional logic operator over implication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpororb 41010	Factor conditional logic operator over disjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ∨ 𝜒), (𝜃 ∨ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∨ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpananb 41011	Factor conditional logic operator over conjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ∧ 𝜒), (𝜃 ∧ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∧ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpnannanb 41012	Factor conditional logic operator over nand in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ⊼ 𝜒), (𝜃 ⊼ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊼ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpor123g 41013	Disjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜏) ∨ if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 ∨ 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 ∨ 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜂)))))
Theorem	ifpimim 41014	Consequnce of implication. (Contributed by RP, 17-Apr-2020.)
⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpbibib 41015	Factor conditional logic operator over biconditional in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ↔ 𝜒), (𝜃 ↔ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ↔ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpxorxorb 41016	Factor conditional logic operator over xor in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ⊻ 𝜒), (𝜃 ⊻ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊻ if-(𝜑, 𝜒, 𝜏)))
20.31.1.2  Sophisms
Theorem	rp-fakeimass 41017	A special case where implication appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020.)
⊢ ((𝜑 ∨ 𝜒) ↔ (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))))
Theorem	rp-fakeanorass 41018	A special case where a mixture of and and or appears to conform to a mixed associative law. (Contributed by RP, 26-Feb-2020.)
⊢ ((𝜒 → 𝜑) ↔ (((𝜑 ∧ 𝜓) ∨ 𝜒) ↔ (𝜑 ∧ (𝜓 ∨ 𝜒))))
Theorem	rp-fakeoranass 41019	A special case where a mixture of or and and appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020.)
⊢ ((𝜑 → 𝜒) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒))))
Theorem	rp-fakeinunass 41020	A special case where a mixture of intersection and union appears to conform to a mixed associative law. (Contributed by RP, 26-Feb-2020.)
⊢ (𝐶 ⊆ 𝐴 ↔ ((𝐴 ∩ 𝐵) ∪ 𝐶) = (𝐴 ∩ (𝐵 ∪ 𝐶)))
Theorem	rp-fakeuninass 41021	A special case where a mixture of union and intersection appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020.)
⊢ (𝐴 ⊆ 𝐶 ↔ ((𝐴 ∪ 𝐵) ∩ 𝐶) = (𝐴 ∪ (𝐵 ∩ 𝐶)))
20.31.1.3  Finite Sets Membership in the class of finite sets can be expressed in many ways.
Theorem	rp-isfinite5 41022*	A set is said to be finite if it can be put in one-to-one correspondence with all the natural numbers between 1 and some 𝑛 ∈ ℕ0. (Contributed by RP, 3-Mar-2020.)
⊢ (𝐴 ∈ Fin ↔ ∃𝑛 ∈ ℕ0 (1...𝑛) ≈ 𝐴)
Theorem	rp-isfinite6 41023*	A set is said to be finite if it is either empty or it can be put in one-to-one correspondence with all the natural numbers between 1 and some 𝑛 ∈ ℕ. (Contributed by RP, 10-Mar-2020.)
⊢ (𝐴 ∈ Fin ↔ (𝐴 = ∅ ∨ ∃𝑛 ∈ ℕ (1...𝑛) ≈ 𝐴))
20.31.1.4  General Observations
Theorem	intabssd 41024*	When for each element 𝑦 there is a subset 𝐴 which may substituted for 𝑥 such that 𝑦 satisfying 𝜒 implies 𝑥 satisfies 𝜓 then the intersection of all 𝑥 that satisfy 𝜓 is a subclass the intersection of all 𝑦 that satisfy 𝜒. (Contributed by RP, 17-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑦)    ⇒   ⊢ (𝜑 → ∩ {𝑥 ∣ 𝜓} ⊆ ∩ {𝑦 ∣ 𝜒})
Theorem	eu0 41025*	There is only one empty set. (Contributed by RP, 1-Oct-2023.)
⊢ (∀𝑥 ¬ 𝑥 ∈ ∅ ∧ ∃!𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	epelon2 41026	Over the ordinal numbers, one may define the relation 𝐴 E 𝐵 iff 𝐴 ∈ 𝐵 and one finds that, under this ordering, On is a well-ordered class, see epweon 7603. This is a weak form of epelg 5487 which only requires that we know 𝐵 to be a set. (Contributed by RP, 27-Sep-2023.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵))
Theorem	ontric3g 41027*	For all 𝑥, 𝑦 ∈ On, one and only one of the following hold: 𝑥 ∈ 𝑦, 𝑦 = 𝑥, or 𝑦 ∈ 𝑥. This is a transparent strict trichotomy. (Contributed by RP, 27-Sep-2023.)
⊢ ∀𝑥 ∈ On ∀𝑦 ∈ On ((𝑥 ∈ 𝑦 ↔ ¬ (𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥)) ∧ (𝑦 = 𝑥 ↔ ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥)) ∧ (𝑦 ∈ 𝑥 ↔ ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 = 𝑥)))
Theorem	dfsucon 41028*	𝐴 is called a successor ordinal if it is not a limit ordinal and not the empty set. (Contributed by RP, 11-Nov-2023.)
⊢ ((Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ ∃𝑥 ∈ On 𝐴 = suc 𝑥)
Theorem	snen1g 41029	A singleton is equinumerous to ordinal one iff its content is a set. (Contributed by RP, 8-Oct-2023.)
⊢ ({𝐴} ≈ 1o ↔ 𝐴 ∈ V)
Theorem	snen1el 41030	A singleton is equinumerous to ordinal one if its content is an element of it. (Contributed by RP, 8-Oct-2023.)
⊢ ({𝐴} ≈ 1o ↔ 𝐴 ∈ {𝐴})
Theorem	sn1dom 41031	A singleton is dominated by ordinal one. (Contributed by RP, 29-Oct-2023.)
⊢ {𝐴} ≼ 1o
Theorem	pr2dom 41032	An unordered pair is dominated by ordinal two. (Contributed by RP, 29-Oct-2023.)
⊢ {𝐴, 𝐵} ≼ 2o
Theorem	tr3dom 41033	An unordered triple is dominated by ordinal three. (Contributed by RP, 29-Oct-2023.)
⊢ {𝐴, 𝐵, 𝐶} ≼ 3o
Theorem	ensucne0 41034	A class equinumerous to a successor is never empty. (Contributed by RP, 11-Nov-2023.) (Proof shortened by SN, 16-Nov-2023.)
⊢ (𝐴 ≈ suc 𝐵 → 𝐴 ≠ ∅)
Theorem	ensucne0OLD 41035	A class equinumerous to a successor is never empty. (Contributed by RP, 11-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≈ suc 𝐵 → 𝐴 ≠ ∅)
Theorem	dfom6 41036	Let ω be defined to be the union of the set of all finite ordinals. (Contributed by RP, 27-Sep-2023.)
⊢ ω = ∪ (On ∩ Fin)
Theorem	infordmin 41037	ω is the smallest infinite ordinal. (Contributed by RP, 27-Sep-2023.)
⊢ ∀𝑥 ∈ (On ∖ Fin)ω ⊆ 𝑥
Theorem	iscard4 41038	Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.)
⊢ ((card‘𝐴) = 𝐴 ↔ 𝐴 ∈ ran card)
Theorem	iscard5 41039*	Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.)
⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴))
Theorem	elrncard 41040*	Let us define a cardinal number to be an element 𝐴 ∈ On such that 𝐴 is not equipotent with any 𝑥 ∈ 𝐴. (Contributed by RP, 1-Oct-2023.)
⊢ (𝐴 ∈ ran card ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴))
Theorem	harval3 41041*	(har‘𝐴) is the least cardinal that is greater than 𝐴. (Contributed by RP, 4-Nov-2023.)
⊢ (𝐴 ∈ dom card → (har‘𝐴) = ∩ {𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥})
Theorem	harval3on 41042*	For any ordinal number 𝐴 let (har‘𝐴) denote the least cardinal that is greater than 𝐴. (Contributed by RP, 4-Nov-2023.)
⊢ (𝐴 ∈ On → (har‘𝐴) = ∩ {𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥})
Theorem	en2pr 41043*	A class is equinumerous to ordinal two iff it is a pair of distinct sets. (Contributed by RP, 11-Oct-2023.)
⊢ (𝐴 ≈ 2o ↔ ∃𝑥∃𝑦(𝐴 = {𝑥, 𝑦} ∧ 𝑥 ≠ 𝑦))
Theorem	pr2cv 41044	If an unordered pair is equinumerous to ordinal two, then both parts are sets. (Contributed by RP, 8-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	pr2el1 41045	If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ {𝐴, 𝐵})
Theorem	pr2cv1 41046	If an unordered pair is equinumerous to ordinal two, then a part is a set. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ V)
Theorem	pr2el2 41047	If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ {𝐴, 𝐵})
Theorem	pr2cv2 41048	If an unordered pair is equinumerous to ordinal two, then a part is a set. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ V)
Theorem	pren2 41049	An unordered pair is equinumerous to ordinal two iff both parts are sets not equal to each other. (Contributed by RP, 8-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵))
Theorem	pr2eldif1 41050	If an unordered pair is equinumerous to ordinal two, then a part is an element of the difference of the pair and the singleton of the other part. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ ({𝐴, 𝐵} ∖ {𝐵}))
Theorem	pr2eldif2 41051	If an unordered pair is equinumerous to ordinal two, then a part is an element of the difference of the pair and the singleton of the other part. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ ({𝐴, 𝐵} ∖ {𝐴}))
Theorem	pren2d 41052	A pair of two distinct sets is equinumerous to ordinal two. (Contributed by RP, 21-Oct-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o)
Theorem	aleph1min 41053	(ℵ‘1o) is the least uncountable ordinal. (Contributed by RP, 18-Nov-2023.)
⊢ (ℵ‘1o) = ∩ {𝑥 ∈ On ∣ ω ≺ 𝑥}
Theorem	alephiso2 41054	ℵ is a strictly order-preserving mapping of On onto the class of all infinite cardinal numbers. (Contributed by RP, 18-Nov-2023.)
⊢ ℵ Isom E , ≺ (On, {𝑥 ∈ ran card ∣ ω ⊆ 𝑥})
Theorem	alephiso3 41055	ℵ is a strictly order-preserving mapping of On onto the class of all infinite cardinal numbers. (Contributed by RP, 18-Nov-2023.)
⊢ ℵ Isom E , ≺ (On, (ran card ∖ ω))
20.31.1.5  Infinite Sets
Theorem	pwelg 41056*	The powerclass is an element of a class closed under union and powerclass operations iff the element is a member of that class. (Contributed by RP, 21-Mar-2020.)
⊢ (∀𝑥 ∈ 𝐵 (∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵) → (𝐴 ∈ 𝐵 ↔ 𝒫 𝐴 ∈ 𝐵))
Theorem	pwinfig 41057*	The powerclass of an infinite set is an infinite set, and vice-versa. Here 𝐵 is a class which is closed under both the union and the powerclass operations and which may have infinite sets as members. (Contributed by RP, 21-Mar-2020.)
⊢ (∀𝑥 ∈ 𝐵 (∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵) → (𝐴 ∈ (𝐵 ∖ Fin) ↔ 𝒫 𝐴 ∈ (𝐵 ∖ Fin)))
Theorem	pwinfi2 41058	The powerclass of an infinite set is an infinite set, and vice-versa. Here 𝑈 is a weak universe. (Contributed by RP, 21-Mar-2020.)
⊢ (𝑈 ∈ WUni → (𝐴 ∈ (𝑈 ∖ Fin) ↔ 𝒫 𝐴 ∈ (𝑈 ∖ Fin)))
Theorem	pwinfi3 41059	The powerclass of an infinite set is an infinite set, and vice-versa. Here 𝑇 is a transitive Tarski universe. (Contributed by RP, 21-Mar-2020.)
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇) → (𝐴 ∈ (𝑇 ∖ Fin) ↔ 𝒫 𝐴 ∈ (𝑇 ∖ Fin)))
Theorem	pwinfi 41060	The powerclass of an infinite set is an infinite set, and vice-versa. (Contributed by RP, 21-Mar-2020.)
⊢ (𝐴 ∈ (V ∖ Fin) ↔ 𝒫 𝐴 ∈ (V ∖ Fin))
20.31.1.6  Finite intersection property While there is not yet a definition, the finite intersection property of a class is introduced by fiint 9021 where two textbook definitions are shown to be equivalent. This property is seen often with ordinal numbers (onin 6282, ordelinel 6349), chains of sets ordered by the proper subset relation (sorpssin 7562), various sets in the field of topology (inopn 21956, incld 22102, innei 22184, ... ) and "universal" classes like weak universes (wunin 10400, tskin 10446) and the class of all sets (inex1g 5238).
Theorem	fipjust 41061*	A definition of the finite intersection property of a class based on closure under pairwise intersection of its elements is independent of the dummy variables. (Contributed by RP, 1-Jan-2020.)
⊢ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 ∩ 𝑣) ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴)
Theorem	cllem0 41062*	The class of all sets with property 𝜑(𝑧) is closed under the binary operation on sets defined in 𝑅(𝑥, 𝑦). (Contributed by RP, 3-Jan-2020.)
⊢ 𝑉 = {𝑧 ∣ 𝜑}    &   ⊢ 𝑅 ∈ 𝑈    &   ⊢ (𝑧 = 𝑅 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑧 = 𝑥 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜓)    ⇒   ⊢ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑅 ∈ 𝑉
Theorem	superficl 41063*	The class of all supersets of a class has the finite intersection property. (Contributed by RP, 1-Jan-2020.) (Proof shortened by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝐵 ⊆ 𝑧}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴
Theorem	superuncl 41064*	The class of all supersets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝐵 ⊆ 𝑧}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴
Theorem	ssficl 41065*	The class of all subsets of a class has the finite intersection property. (Contributed by RP, 1-Jan-2020.) (Proof shortened by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴
Theorem	ssuncl 41066*	The class of all subsets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴
Theorem	ssdifcl 41067*	The class of all subsets of a class is closed under class difference. (Contributed by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∖ 𝑦) ∈ 𝐴
Theorem	sssymdifcl 41068*	The class of all subsets of a class is closed under symmetric difference. (Contributed by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∖ 𝑦) ∪ (𝑦 ∖ 𝑥)) ∈ 𝐴
Theorem	fiinfi 41069*	If two classes have the finite intersection property, then so does their intersection. (Contributed by RP, 1-Jan-2020.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 = (𝐴 ∩ 𝐵))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥 ∩ 𝑦) ∈ 𝐶)
20.31.1.7  RP ADDTO: Subclasses and subsets
Theorem	rababg 41070	Condition when restricted class is equal to unrestricted class. (Contributed by RP, 13-Aug-2020.)
⊢ (∀𝑥(𝜑 → 𝑥 ∈ 𝐴) ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑})
20.31.1.8  RP ADDTO: The intersection of a class
Theorem	elintabg 41071*	Two ways of saying a set is an element of the intersection of a class. (Contributed by RP, 13-Aug-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)))
Theorem	elinintab 41072*	Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 13-Aug-2020.)
⊢ (𝐴 ∈ (𝐵 ∩ ∩ {𝑥 ∣ 𝜑}) ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)))
Theorem	elmapintrab 41073*	Two ways to say a set is an element of the intersection of a class of images. (Contributed by RP, 16-Aug-2020.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐶 ⊆ 𝐵    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑤 ∈ 𝒫 𝐵 ∣ ∃𝑥(𝑤 = 𝐶 ∧ 𝜑)} ↔ ((∃𝑥𝜑 → 𝐴 ∈ 𝐵) ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝐶))))
20.31.1.9  RP ADDTO: Theorems requiring subset and intersection existence
Theorem	elinintrab 41074*	Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 14-Aug-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑤 ∈ 𝒫 𝐵 ∣ ∃𝑥(𝑤 = (𝐵 ∩ 𝑥) ∧ 𝜑)} ↔ ((∃𝑥𝜑 → 𝐴 ∈ 𝐵) ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))))
Theorem	inintabss 41075*	Upper bound on intersection of class and the intersection of a class. (Contributed by RP, 13-Aug-2020.)
⊢ (𝐴 ∩ ∩ {𝑥 ∣ 𝜑}) ⊆ ∩ {𝑤 ∈ 𝒫 𝐴 ∣ ∃𝑥(𝑤 = (𝐴 ∩ 𝑥) ∧ 𝜑)}
Theorem	inintabd 41076*	Value of the intersection of class with the intersection of a nonempty class. (Contributed by RP, 13-Aug-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → (𝐴 ∩ ∩ {𝑥 ∣ 𝜓}) = ∩ {𝑤 ∈ 𝒫 𝐴 ∣ ∃𝑥(𝑤 = (𝐴 ∩ 𝑥) ∧ 𝜓)})
20.31.1.10  RP ADDTO: Relations
Theorem	xpinintabd 41077*	Value of the intersection of Cartesian product with the intersection of a nonempty class. (Contributed by RP, 12-Aug-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → ((𝐴 × 𝐵) ∩ ∩ {𝑥 ∣ 𝜓}) = ∩ {𝑤 ∈ 𝒫 (𝐴 × 𝐵) ∣ ∃𝑥(𝑤 = ((𝐴 × 𝐵) ∩ 𝑥) ∧ 𝜓)})
Theorem	relintabex 41078	If the intersection of a class is a relation, then the class is nonempty. (Contributed by RP, 12-Aug-2020.)
⊢ (Rel ∩ {𝑥 ∣ 𝜑} → ∃𝑥𝜑)
Theorem	elcnvcnvintab 41079*	Two ways of saying a set is an element of the converse of the converse of the intersection of a class. (Contributed by RP, 20-Aug-2020.)
⊢ (𝐴 ∈ ◡◡∩ {𝑥 ∣ 𝜑} ↔ (𝐴 ∈ (V × V) ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)))
Theorem	relintab 41080*	Value of the intersection of a class when it is a relation. (Contributed by RP, 12-Aug-2020.)
⊢ (Rel ∩ {𝑥 ∣ 𝜑} → ∩ {𝑥 ∣ 𝜑} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)})
Theorem	nonrel 41081	A non-relation is equal to the base class with all ordered pairs removed. (Contributed by RP, 25-Oct-2020.)
⊢ (𝐴 ∖ ◡◡𝐴) = (𝐴 ∖ (V × V))
Theorem	elnonrel 41082	Only an ordered pair where not both entries are sets could be an element of the non-relation part of class. (Contributed by RP, 25-Oct-2020.)
⊢ (⟨𝑋, 𝑌⟩ ∈ (𝐴 ∖ ◡◡𝐴) ↔ (∅ ∈ 𝐴 ∧ ¬ (𝑋 ∈ V ∧ 𝑌 ∈ V)))
Theorem	cnvssb 41083	Subclass theorem for converse. (Contributed by RP, 22-Oct-2020.)
⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ◡𝐴 ⊆ ◡𝐵))
Theorem	relnonrel 41084	The non-relation part of a relation is empty. (Contributed by RP, 22-Oct-2020.)
⊢ (Rel 𝐴 ↔ (𝐴 ∖ ◡◡𝐴) = ∅)
Theorem	cnvnonrel 41085	The converse of the non-relation part of a class is empty. (Contributed by RP, 18-Oct-2020.)
⊢ ◡(𝐴 ∖ ◡◡𝐴) = ∅
Theorem	brnonrel 41086	A non-relation cannot relate any two classes. (Contributed by RP, 23-Oct-2020.)
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → ¬ 𝑋(𝐴 ∖ ◡◡𝐴)𝑌)
Theorem	dmnonrel 41087	The domain of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ dom (𝐴 ∖ ◡◡𝐴) = ∅
Theorem	rnnonrel 41088	The range of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ran (𝐴 ∖ ◡◡𝐴) = ∅
Theorem	resnonrel 41089	A restriction of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ((𝐴 ∖ ◡◡𝐴) ↾ 𝐵) = ∅
Theorem	imanonrel 41090	An image under the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ((𝐴 ∖ ◡◡𝐴) “ 𝐵) = ∅
Theorem	cononrel1 41091	Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ((𝐴 ∖ ◡◡𝐴) ∘ 𝐵) = ∅
Theorem	cononrel2 41092	Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ (𝐴 ∘ (𝐵 ∖ ◡◡𝐵)) = ∅
20.31.1.11  RP ADDTO: Functions See also idssxp 5945 by Thierry Arnoux.
Theorem	elmapintab 41093*	Two ways to say a set is an element of mapped intersection of a class. Here 𝐹 maps elements of 𝐶 to elements of ∩ {𝑥 ∣ 𝜑} or 𝑥. (Contributed by RP, 19-Aug-2020.)
⊢ (𝐴 ∈ 𝐵 ↔ (𝐴 ∈ 𝐶 ∧ (𝐹‘𝐴) ∈ ∩ {𝑥 ∣ 𝜑}))    &   ⊢ (𝐴 ∈ 𝐸 ↔ (𝐴 ∈ 𝐶 ∧ (𝐹‘𝐴) ∈ 𝑥))    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ (𝐴 ∈ 𝐶 ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝐸)))
Theorem	fvnonrel 41094	The function value of any class under a non-relation is empty. (Contributed by RP, 23-Oct-2020.)
⊢ ((𝐴 ∖ ◡◡𝐴)‘𝑋) = ∅
Theorem	elinlem 41095	Two ways to say a set is a member of an intersection. (Contributed by RP, 19-Aug-2020.)
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ( I ‘𝐴) ∈ 𝐶))
Theorem	elcnvcnvlem 41096	Two ways to say a set is a member of the converse of the converse of a class. (Contributed by RP, 20-Aug-2020.)
⊢ (𝐴 ∈ ◡◡𝐵 ↔ (𝐴 ∈ (V × V) ∧ ( I ‘𝐴) ∈ 𝐵))
20.31.1.12  RP ADDTO: Finite induction (for finite ordinals) Original probably needs new subsection for Relation-related existence theorems.
Theorem	cnvcnvintabd 41097*	Value of the relationship content of the intersection of a class. (Contributed by RP, 20-Aug-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → ◡◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜓)})
20.31.1.13  RP ADDTO: First and second members of an ordered pair
Theorem	elcnvlem 41098	Two ways to say a set is a member of the converse of a class. (Contributed by RP, 19-Aug-2020.)
⊢ 𝐹 = (𝑥 ∈ (V × V) ↦ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)    ⇒   ⊢ (𝐴 ∈ ◡𝐵 ↔ (𝐴 ∈ (V × V) ∧ (𝐹‘𝐴) ∈ 𝐵))
Theorem	elcnvintab 41099*	Two ways of saying a set is an element of the converse of the intersection of a class. (Contributed by RP, 19-Aug-2020.)
⊢ (𝐴 ∈ ◡∩ {𝑥 ∣ 𝜑} ↔ (𝐴 ∈ (V × V) ∧ ∀𝑥(𝜑 → 𝐴 ∈ ◡𝑥)))
Theorem	cnvintabd 41100*	Value of the converse of the intersection of a nonempty class. (Contributed by RP, 20-Aug-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → ◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡𝑥 ∧ 𝜓)})