P. 437 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43601-43700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ifpid1g 43601	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((𝜒 → 𝜑) ∧ (𝜑 → 𝜓)))
Theorem	ifpim23g 43602	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ (((𝜑 → 𝜓) ↔ if-(𝜒, 𝜓, ¬ 𝜑)) ↔ (((𝜑 ∧ 𝜓) → 𝜒) ∧ (𝜒 → (𝜑 ∨ 𝜓))))
Theorem	ifpim3 43603	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ ((𝜑 → 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜑))
Theorem	ifpnim1 43604	Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜑))
Theorem	ifpim4 43605	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, 𝜓, ¬ 𝜑))
Theorem	ifpnim2 43606	Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜓, ¬ 𝜓, 𝜑))
Theorem	ifpim123g 43607	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 43608	Implication of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)) ↔ (((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)) ∧ ((𝜑 → 𝜓) ∨ (𝜒 → 𝜃))))
Theorem	ifp1bi 43609	Substitute the first element of conditional logical operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃)) ↔ ((((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜑 → 𝜓) ∨ (𝜃 → 𝜒))) ∧ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)))))
Theorem	ifpbi1b 43610	When the first variable is irrelevant, it can be replaced. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, 𝜒, 𝜒) ↔ if-(𝜓, 𝜒, 𝜒))
Theorem	ifpimimb 43611	Factor conditional logic operator over implication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpororb 43612	Factor conditional logic operator over disjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ∨ 𝜒), (𝜃 ∨ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∨ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpananb 43613	Factor conditional logic operator over conjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ∧ 𝜒), (𝜃 ∧ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∧ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpnannanb 43614	Factor conditional logic operator over nand in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ⊼ 𝜒), (𝜃 ⊼ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊼ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpor123g 43615	Disjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜏) ∨ if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 ∨ 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 ∨ 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜂)))))
Theorem	ifpimim 43616	Consequnce of implication. (Contributed by RP, 17-Apr-2020.)
⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpbibib 43617	Factor conditional logic operator over biconditional in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ↔ 𝜒), (𝜃 ↔ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ↔ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpxorxorb 43618	Factor conditional logic operator over xor in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ⊻ 𝜒), (𝜃 ⊻ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊻ if-(𝜑, 𝜒, 𝜏)))
21.36.4.2  Sophisms
Theorem	rp-fakeimass 43619	A special case where implication appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020.)
⊢ ((𝜑 ∨ 𝜒) ↔ (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))))
Theorem	rp-fakeanorass 43620	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 43621	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 43622	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 43623	A special case where a mixture of union and intersection appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020.)
⊢ (𝐴 ⊆ 𝐶 ↔ ((𝐴 ∪ 𝐵) ∩ 𝐶) = (𝐴 ∪ (𝐵 ∩ 𝐶)))
21.36.4.3  Finite Sets Membership in the class of finite sets can be expressed in many ways.
Theorem	rp-isfinite5 43624*	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 43625*	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...𝑛) ≈ 𝐴))
21.36.4.4  General Observations
Theorem	intabssd 43626*	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 43627*	There is only one empty set. (Contributed by RP, 1-Oct-2023.)
⊢ (∀𝑥 ¬ 𝑥 ∈ ∅ ∧ ∃!𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	epelon2 43628	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 7717. This is a weak form of epelg 5522 which only requires that we know 𝐵 to be a set. (Contributed by RP, 27-Sep-2023.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵))
Theorem	ontric3g 43629*	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 43630*	𝐴 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 43631	A singleton is equinumerous to ordinal one iff its content is a set. (Contributed by RP, 8-Oct-2023.)
⊢ ({𝐴} ≈ 1o ↔ 𝐴 ∈ V)
Theorem	snen1el 43632	A singleton is equinumerous to ordinal one if its content is an element of it. (Contributed by RP, 8-Oct-2023.)
⊢ ({𝐴} ≈ 1o ↔ 𝐴 ∈ {𝐴})
Theorem	sn1dom 43633	A singleton is dominated by ordinal one. (Contributed by RP, 29-Oct-2023.)
⊢ {𝐴} ≼ 1o
Theorem	pr2dom 43634	An unordered pair is dominated by ordinal two. (Contributed by RP, 29-Oct-2023.)
⊢ {𝐴, 𝐵} ≼ 2o
Theorem	tr3dom 43635	An unordered triple is dominated by ordinal three. (Contributed by RP, 29-Oct-2023.)
⊢ {𝐴, 𝐵, 𝐶} ≼ 3o
Theorem	ensucne0 43636	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 43637	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 43638	Let ω be defined to be the union of the set of all finite ordinals. (Contributed by RP, 27-Sep-2023.)
⊢ ω = ∪ (On ∩ Fin)
Theorem	infordmin 43639	ω is the smallest infinite ordinal. (Contributed by RP, 27-Sep-2023.)
⊢ ∀𝑥 ∈ (On ∖ Fin)ω ⊆ 𝑥
Theorem	iscard4 43640	Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.)
⊢ ((card‘𝐴) = 𝐴 ↔ 𝐴 ∈ ran card)
Theorem	minregex 43641*	Given any cardinal number 𝐴, there exists an argument 𝑥, which yields the least regular uncountable value of ℵ which is greater to or equal to 𝐴. This proof uses AC. (Contributed by RP, 23-Nov-2023.)
⊢ (𝐴 ∈ (ran card ∖ ω) → ∃𝑥 ∈ On 𝑥 = ∩ {𝑦 ∈ On ∣ (∅ ∈ 𝑦 ∧ 𝐴 ⊆ (ℵ‘𝑦) ∧ (cf‘(ℵ‘𝑦)) = (ℵ‘𝑦))})
Theorem	minregex2 43642*	Given any cardinal number 𝐴, there exists an argument 𝑥, which yields the least regular uncountable value of ℵ which dominates 𝐴. This proof uses AC. (Contributed by RP, 24-Nov-2023.)
⊢ (𝐴 ∈ (ran card ∖ ω) → ∃𝑥 ∈ On 𝑥 = ∩ {𝑦 ∈ On ∣ (∅ ∈ 𝑦 ∧ 𝐴 ≼ (ℵ‘𝑦) ∧ (cf‘(ℵ‘𝑦)) = (ℵ‘𝑦))})
Theorem	iscard5 43643*	Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.)
⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴))
Theorem	elrncard 43644*	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 43645*	(har‘𝐴) is the least cardinal that is greater than 𝐴. (Contributed by RP, 4-Nov-2023.)
⊢ (𝐴 ∈ dom card → (har‘𝐴) = ∩ {𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥})
Theorem	harval3on 43646*	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	omssrncard 43647	All natural numbers are cardinals. (Contributed by RP, 1-Oct-2023.)
⊢ ω ⊆ ran card
Theorem	0iscard 43648	0 is a cardinal number. (Contributed by RP, 1-Oct-2023.)
⊢ ∅ ∈ ran card
Theorem	1iscard 43649	1 is a cardinal number. (Contributed by RP, 1-Oct-2023.)
⊢ 1o ∈ ran card
Theorem	omiscard 43650	ω is a cardinal number. (Contributed by RP, 1-Oct-2023.)
⊢ ω ∈ ran card
Theorem	sucomisnotcard 43651	ω +o 1o is not a cardinal number. (Contributed by RP, 1-Oct-2023.)
⊢ ¬ (ω +o 1o) ∈ ran card
Theorem	nna1iscard 43652	For any natural number, the add one operation is results in a cardinal number. (Contributed by RP, 1-Oct-2023.)
⊢ (𝑁 ∈ ω → (𝑁 +o 1o) ∈ ran card)
Theorem	har2o 43653	The least cardinal greater than 2 is 3. (Contributed by RP, 5-Nov-2023.)
⊢ (har‘2o) = 3o
Theorem	en2pr 43654*	A class is equinumerous to ordinal two iff it is a pair of distinct sets. (Contributed by RP, 11-Oct-2023.)
⊢ (𝐴 ≈ 2o ↔ ∃𝑥∃𝑦(𝐴 = {𝑥, 𝑦} ∧ 𝑥 ≠ 𝑦))
Theorem	pr2cv 43655	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 43656	If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ {𝐴, 𝐵})
Theorem	pr2cv1 43657	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 43658	If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ {𝐴, 𝐵})
Theorem	pr2cv2 43659	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 43660	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 43661	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 43662	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 43663	A pair of two distinct sets is equinumerous to ordinal two. (Contributed by RP, 21-Oct-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o)
Theorem	aleph1min 43664	(ℵ‘1o) is the least uncountable ordinal. (Contributed by RP, 18-Nov-2023.)
⊢ (ℵ‘1o) = ∩ {𝑥 ∈ On ∣ ω ≺ 𝑥}
Theorem	alephiso2 43665	ℵ 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 43666	ℵ 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 ∖ ω))
21.36.4.5  Infinite Sets
Theorem	pwelg 43667*	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 43668*	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 43669	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 43670	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 43671	The powerclass of an infinite set is an infinite set, and vice-versa. (Contributed by RP, 21-Mar-2020.)
⊢ (𝐴 ∈ (V ∖ Fin) ↔ 𝒫 𝐴 ∈ (V ∖ Fin))
21.36.4.6  Finite intersection property While there is not yet a definition, the finite intersection property of a class is introduced by fiint 9221 where two textbook definitions are shown to be equivalent. This property is seen often with ordinal numbers (onin 6345, ordelinel 6417), chains of sets ordered by the proper subset relation (sorpssin 7673), various sets in the field of topology (inopn 22824, incld 22968, innei 23050, ... ) and "universal" classes like weak universes (wunin 10614, tskin 10660) and the class of all sets (inex1g 5261).
Theorem	fipjust 43672*	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 43673*	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 43674*	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 43675*	The class of all supersets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝐵 ⊆ 𝑧}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴
Theorem	ssficl 43676*	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 43677*	The class of all subsets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴
Theorem	ssdifcl 43678*	The class of all subsets of a class is closed under class difference. (Contributed by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∖ 𝑦) ∈ 𝐴
Theorem	sssymdifcl 43679*	The class of all subsets of a class is closed under symmetric difference. (Contributed by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∖ 𝑦) ∪ (𝑦 ∖ 𝑥)) ∈ 𝐴
Theorem	fiinfi 43680*	If two classes have the finite intersection property, then so does their intersection. (Contributed by RP, 1-Jan-2020.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 = (𝐴 ∩ 𝐵))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥 ∩ 𝑦) ∈ 𝐶)
21.36.4.7  RP ADDTO: Subclasses and subsets
Theorem	rababg 43681	Condition when restricted class is equal to unrestricted class. (Contributed by RP, 13-Aug-2020.)
⊢ (∀𝑥(𝜑 → 𝑥 ∈ 𝐴) ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑})
21.36.4.8  RP ADDTO: The intersection of a class
Theorem	elinintab 43682*	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 43683*	Two ways to say a set is an element of the intersection of a class of images. (Contributed by RP, 16-Aug-2020.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐶 ⊆ 𝐵    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑤 ∈ 𝒫 𝐵 ∣ ∃𝑥(𝑤 = 𝐶 ∧ 𝜑)} ↔ ((∃𝑥𝜑 → 𝐴 ∈ 𝐵) ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝐶))))
21.36.4.9  RP ADDTO: Theorems requiring subset and intersection existence
Theorem	elinintrab 43684*	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 43685*	Upper bound on intersection of class and the intersection of a class. (Contributed by RP, 13-Aug-2020.)
⊢ (𝐴 ∩ ∩ {𝑥 ∣ 𝜑}) ⊆ ∩ {𝑤 ∈ 𝒫 𝐴 ∣ ∃𝑥(𝑤 = (𝐴 ∩ 𝑥) ∧ 𝜑)}
Theorem	inintabd 43686*	Value of the intersection of class with the intersection of a nonempty class. (Contributed by RP, 13-Aug-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → (𝐴 ∩ ∩ {𝑥 ∣ 𝜓}) = ∩ {𝑤 ∈ 𝒫 𝐴 ∣ ∃𝑥(𝑤 = (𝐴 ∩ 𝑥) ∧ 𝜓)})
21.36.4.10  RP ADDTO: Relations
Theorem	xpinintabd 43687*	Value of the intersection of Cartesian product with the intersection of a nonempty class. (Contributed by RP, 12-Aug-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → ((𝐴 × 𝐵) ∩ ∩ {𝑥 ∣ 𝜓}) = ∩ {𝑤 ∈ 𝒫 (𝐴 × 𝐵) ∣ ∃𝑥(𝑤 = ((𝐴 × 𝐵) ∩ 𝑥) ∧ 𝜓)})
Theorem	relintabex 43688	If the intersection of a class is a relation, then the class is nonempty. (Contributed by RP, 12-Aug-2020.)
⊢ (Rel ∩ {𝑥 ∣ 𝜑} → ∃𝑥𝜑)
Theorem	elcnvcnvintab 43689*	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 43690*	Value of the intersection of a class when it is a relation. (Contributed by RP, 12-Aug-2020.)
⊢ (Rel ∩ {𝑥 ∣ 𝜑} → ∩ {𝑥 ∣ 𝜑} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)})
Theorem	nonrel 43691	A non-relation is equal to the base class with all ordered pairs removed. (Contributed by RP, 25-Oct-2020.)
⊢ (𝐴 ∖ ◡◡𝐴) = (𝐴 ∖ (V × V))
Theorem	elnonrel 43692	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 43693	Subclass theorem for converse. (Contributed by RP, 22-Oct-2020.)
⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ◡𝐴 ⊆ ◡𝐵))
Theorem	relnonrel 43694	The non-relation part of a relation is empty. (Contributed by RP, 22-Oct-2020.)
⊢ (Rel 𝐴 ↔ (𝐴 ∖ ◡◡𝐴) = ∅)
Theorem	cnvnonrel 43695	The converse of the non-relation part of a class is empty. (Contributed by RP, 18-Oct-2020.)
⊢ ◡(𝐴 ∖ ◡◡𝐴) = ∅
Theorem	brnonrel 43696	A non-relation cannot relate any two classes. (Contributed by RP, 23-Oct-2020.)
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → ¬ 𝑋(𝐴 ∖ ◡◡𝐴)𝑌)
Theorem	dmnonrel 43697	The domain of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ dom (𝐴 ∖ ◡◡𝐴) = ∅
Theorem	rnnonrel 43698	The range of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ran (𝐴 ∖ ◡◡𝐴) = ∅
Theorem	resnonrel 43699	A restriction of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ((𝐴 ∖ ◡◡𝐴) ↾ 𝐵) = ∅
Theorem	imanonrel 43700	An image under the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ((𝐴 ∖ ◡◡𝐴) “ 𝐵) = ∅