P. 432 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43101-43200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bccm1k 43101	Generalized binomial coefficient: 𝐶 choose (𝐾 − 1), when 𝐶 is not (𝐾 − 1). (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ (ℂ ∖ {(𝐾 − 1)}))    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐶C𝑐(𝐾 − 1)) = ((𝐶C𝑐𝐾) / ((𝐶 − (𝐾 − 1)) / 𝐾)))
Theorem	bccn0 43102	Generalized binomial coefficient: 𝐶 choose 0. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐶C𝑐0) = 1)
Theorem	bccn1 43103	Generalized binomial coefficient: 𝐶 choose 1. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐶C𝑐1) = 𝐶)
Theorem	bccbc 43104	The binomial coefficient and generalized binomial coefficient are equal when their arguments are nonnegative integers. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑁C𝑐𝐾) = (𝑁C𝐾))
21.37.7  Binomial series
Theorem	uzmptshftfval 43105*	When 𝐹 is a maps-to function on some set of upper integers 𝑍 that returns a set 𝐵, (𝐹 shift 𝑁) is another maps-to function on the shifted set of upper integers 𝑊. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝑍 ↦ 𝐵)    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 = (𝑦 − 𝑁) → 𝐵 = 𝐶)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐹 shift 𝑁) = (𝑦 ∈ 𝑊 ↦ 𝐶))
Theorem	dvradcnv2 43106*	The radius of convergence of the (formal) derivative 𝐻 of the power series 𝐺 is (at least) as large as the radius of convergence of 𝐺. This version of dvradcnv 25933 uses a shifted version of 𝐻 to match the sum form of (ℂ D 𝐹) in pserdv2 25942 (and shows how to use uzmptshftfval 43105 to shift a maps-to function on a set of upper integers). (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((𝑛 · (𝐴‘𝑛)) · (𝑋↑(𝑛 − 1))))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘𝑋) < 𝑅)    ⇒   ⊢ (𝜑 → seq1( + , 𝐻) ∈ dom ⇝ )
Theorem	binomcxplemwb 43107	Lemma for binomcxp 43116. The lemma in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    ⇒   ⊢ (𝜑 → (((𝐶 − 𝐾) · (𝐶C𝑐𝐾)) + ((𝐶 − (𝐾 − 1)) · (𝐶C𝑐(𝐾 − 1)))) = (𝐶 · (𝐶C𝑐𝐾)))
Theorem	binomcxplemnn0 43108*	Lemma for binomcxp 43116. When 𝐶 is a nonnegative integer, the binomial's finite sum value by the standard binomial theorem binom 15776 equals this generalized infinite sum: the generalized binomial coefficient and exponentiation operators give exactly the same values in the standard index set (0...𝐶), and when the index set is widened beyond 𝐶 the additional values are just zeroes. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴))    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑐𝐶) = Σ𝑘 ∈ ℕ0 ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))))
Theorem	binomcxplemrat 43109*	Lemma for binomcxp 43116. As 𝑘 increases, this ratio's absolute value converges to one. Part of equation "Since continuity of the absolute value..." in the Wikibooks proof (proven for the inverse ratio, which we later show is no problem). (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴))    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (abs‘((𝐶 − 𝑘) / (𝑘 + 1)))) ⇝ 1)
Theorem	binomcxplemfrat 43110*	Lemma for binomcxp 43116. binomcxplemrat 43109 implies that when 𝐶 is not a nonnegative integer, the absolute value of the ratio ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) converges to one. The rest of equation "Since continuity of the absolute value..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴))    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))    ⇒   ⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (𝑘 ∈ ℕ0 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)))) ⇝ 1)
Theorem	binomcxplemradcnv 43111*	Lemma for binomcxp 43116. By binomcxplemfrat 43110 and radcnvrat 43073 the radius of convergence of power series Σ𝑘 ∈ ℕ0((𝐹‘𝑘) · (𝑏↑𝑘)) is one. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴))    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))    &   ⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    ⇒   ⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → 𝑅 = 1)
Theorem	binomcxplemdvbinom 43112*	Lemma for binomcxp 43116. By the power and chain rules, calculate the derivative of ((1 + 𝑏)↑𝑐-𝐶), with respect to 𝑏 in the disk of convergence 𝐷. We later multiply the derivative in the later binomcxplemdvsum 43114 by this derivative to show that ((1 + 𝑏)↑𝑐𝐶) (with a nonnegated 𝐶) and the later sum, since both at 𝑏 = 0 equal one, are the same. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴))    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))    &   ⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1)))))    &   ⊢ 𝐷 = (◡abs “ (0[,)𝑅))    ⇒   ⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ D (𝑏 ∈ 𝐷 ↦ ((1 + 𝑏)↑𝑐-𝐶))) = (𝑏 ∈ 𝐷 ↦ (-𝐶 · ((1 + 𝑏)↑𝑐(-𝐶 − 1)))))
Theorem	binomcxplemcvg 43113*	Lemma for binomcxp 43116. The sum in binomcxplemnn0 43108 and its derivative (see the next theorem, binomcxplemdvsum 43114) converge, as long as their base 𝐽 is within the disk of convergence. Part of remark "This convergence allows us to apply term-by-term differentiation..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴))    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))    &   ⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1)))))    &   ⊢ 𝐷 = (◡abs “ (0[,)𝑅))    ⇒   ⊢ ((𝜑 ∧ 𝐽 ∈ 𝐷) → (seq0( + , (𝑆‘𝐽)) ∈ dom ⇝ ∧ seq1( + , (𝐸‘𝐽)) ∈ dom ⇝ ))
Theorem	binomcxplemdvsum 43114*	Lemma for binomcxp 43116. The derivative of the generalized sum in binomcxplemnn0 43108. Part of remark "This convergence allows to apply term-by-term differentiation..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴))    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))    &   ⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1)))))    &   ⊢ 𝐷 = (◡abs “ (0[,)𝑅))    &   ⊢ 𝑃 = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ0 ((𝑆‘𝑏)‘𝑘))    ⇒   ⊢ (𝜑 → (ℂ D 𝑃) = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ ((𝐸‘𝑏)‘𝑘)))
Theorem	binomcxplemnotnn0 43115*	Lemma for binomcxp 43116. When 𝐶 is not a nonnegative integer, the generalized sum in binomcxplemnn0 43108 —which we will call 𝑃 —is a convergent power series: its base 𝑏 is always of smaller absolute value than the radius of convergence. pserdv2 25942 gives the derivative of 𝑃, which by dvradcnv 25933 also converges in that radius. When 𝐴 is fixed at one, (𝐴 + 𝑏) times that derivative equals (𝐶 · 𝑃) and fraction (𝑃 / ((𝐴 + 𝑏)↑𝑐𝐶)) is always defined with derivative zero, so the fraction is a constant—specifically one, because ((1 + 0)↑𝑐𝐶) = 1. Thus ((1 + 𝑏)↑𝑐𝐶) = (𝑃‘𝑏). Finally, let 𝑏 be (𝐵 / 𝐴), and multiply both the binomial ((1 + (𝐵 / 𝐴))↑𝑐𝐶) and the sum (𝑃‘(𝐵 / 𝐴)) by (𝐴↑𝑐𝐶) to get the result. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴))    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))    &   ⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1)))))    &   ⊢ 𝐷 = (◡abs “ (0[,)𝑅))    &   ⊢ 𝑃 = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ0 ((𝑆‘𝑏)‘𝑘))    ⇒   ⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑐𝐶) = Σ𝑘 ∈ ℕ0 ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))))
Theorem	binomcxp 43116*	Generalize the binomial theorem binom 15776 to positive real summand 𝐴, real summand 𝐵, and complex exponent 𝐶. Proof in https://en.wikibooks.org/wiki/Advanced_Calculus 15776; see also https://en.wikipedia.org/wiki/Binomial_series 15776, https://en.wikipedia.org/wiki/Binomial_theorem 15776 (sections "Newton's generalized binomial theorem" and "Future generalizations"), and proof "General Binomial Theorem" in https://proofwiki.org/wiki/Binomial_Theorem 15776. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴))    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵)↑𝑐𝐶) = Σ𝑘 ∈ ℕ0 ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))))
21.38  Mathbox for Andrew Salmon
21.38.1  Principia Mathematica * 10
Theorem	pm10.12 43117*	Theorem *10.12 in [WhiteheadRussell] p. 146. In *10, this is treated as an axiom, and the proofs in *10 are based on this theorem. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ (∀𝑥(𝜑 ∨ 𝜓) → (𝜑 ∨ ∀𝑥𝜓))
Theorem	pm10.14 43118	Theorem *10.14 in [WhiteheadRussell] p. 146. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
Theorem	pm10.251 43119	Theorem *10.251 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ (∀𝑥 ¬ 𝜑 → ¬ ∀𝑥𝜑)
Theorem	pm10.252 43120	Theorem *10.252 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.) (New usage is discouraged.)
⊢ (¬ ∃𝑥𝜑 ↔ ∀𝑥 ¬ 𝜑)
Theorem	pm10.253 43121	Theorem *10.253 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ (¬ ∀𝑥𝜑 ↔ ∃𝑥 ¬ 𝜑)
Theorem	albitr 43122	Theorem *10.301 in [WhiteheadRussell] p. 151. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∀𝑥(𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜓 ↔ 𝜒)) → ∀𝑥(𝜑 ↔ 𝜒))
Theorem	pm10.42 43123	Theorem *10.42 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ ((∃𝑥𝜑 ∨ ∃𝑥𝜓) ↔ ∃𝑥(𝜑 ∨ 𝜓))
Theorem	pm10.52 43124*	Theorem *10.52 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ 𝜓))
Theorem	pm10.53 43125	Theorem *10.53 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (¬ ∃𝑥𝜑 → ∀𝑥(𝜑 → 𝜓))
Theorem	pm10.541 43126*	Theorem *10.541 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥(𝜑 → (𝜒 ∨ 𝜓)) ↔ (𝜒 ∨ ∀𝑥(𝜑 → 𝜓)))
Theorem	pm10.542 43127*	Theorem *10.542 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥(𝜑 → (𝜒 → 𝜓)) ↔ (𝜒 → ∀𝑥(𝜑 → 𝜓)))
Theorem	pm10.55 43128	Theorem *10.55 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∃𝑥(𝜑 ∧ 𝜓) ∧ ∀𝑥(𝜑 → 𝜓)) ↔ (∃𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓)))
Theorem	pm10.56 43129	Theorem *10.56 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ ∃𝑥(𝜑 ∧ 𝜒)) → ∃𝑥(𝜓 ∧ 𝜒))
Theorem	pm10.57 43130	Theorem *10.57 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥(𝜑 → (𝜓 ∨ 𝜒)) → (∀𝑥(𝜑 → 𝜓) ∨ ∃𝑥(𝜑 ∧ 𝜒)))
21.38.2  Principia Mathematica * 11
Theorem	2alanimi 43131	Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((∀𝑥∀𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓) → ∀𝑥∀𝑦𝜒)
Theorem	2al2imi 43132	Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜒))
Theorem	pm11.11 43133	Theorem *11.11 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ 𝜑    ⇒   ⊢ ∀𝑧∀𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
Theorem	pm11.12 43134*	Theorem *11.12 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ (∀𝑥∀𝑦(𝜑 ∨ 𝜓) → (𝜑 ∨ ∀𝑥∀𝑦𝜓))
Theorem	19.21vv 43135*	Compare Theorem *11.3 in [WhiteheadRussell] p. 161. Special case of theorem 19.21 of [Margaris] p. 90 with two quantifiers. See 19.21v 1943. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦(𝜓 → 𝜑) ↔ (𝜓 → ∀𝑥∀𝑦𝜑))
Theorem	2alim 43136	Theorem *11.32 in [WhiteheadRussell] p. 162. Theorem 19.20 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	2albi 43137	Theorem *11.33 in [WhiteheadRussell] p. 162. Theorem 19.15 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓))
Theorem	2exim 43138	Theorem *11.34 in [WhiteheadRussell] p. 162. Theorem 19.22 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓))
Theorem	2exbi 43139	Theorem *11.341 in [WhiteheadRussell] p. 162. Theorem 19.18 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓))
Theorem	spsbce-2 43140	Theorem *11.36 in [WhiteheadRussell] p. 162. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑥∃𝑦𝜑)
Theorem	19.33-2 43141	Theorem *11.421 in [WhiteheadRussell] p. 163. Theorem 19.33 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∀𝑥∀𝑦𝜑 ∨ ∀𝑥∀𝑦𝜓) → ∀𝑥∀𝑦(𝜑 ∨ 𝜓))
Theorem	19.36vv 43142*	Theorem *11.43 in [WhiteheadRussell] p. 163. Theorem 19.36 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 25-May-2011.)
⊢ (∃𝑥∃𝑦(𝜑 → 𝜓) ↔ (∀𝑥∀𝑦𝜑 → 𝜓))
Theorem	19.31vv 43143*	Theorem *11.44 in [WhiteheadRussell] p. 163. Theorem 19.31 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦(𝜑 ∨ 𝜓) ↔ (∀𝑥∀𝑦𝜑 ∨ 𝜓))
Theorem	19.37vv 43144*	Theorem *11.46 in [WhiteheadRussell] p. 164. Theorem 19.37 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥∃𝑦(𝜓 → 𝜑) ↔ (𝜓 → ∃𝑥∃𝑦𝜑))
Theorem	19.28vv 43145*	Theorem *11.47 in [WhiteheadRussell] p. 164. Theorem 19.28 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦(𝜓 ∧ 𝜑) ↔ (𝜓 ∧ ∀𝑥∀𝑦𝜑))
Theorem	pm11.52 43146	Theorem *11.52 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ¬ ∀𝑥∀𝑦(𝜑 → ¬ 𝜓))
Theorem	aaanv 43147*	Theorem *11.56 in [WhiteheadRussell] p. 165. Special case of aaan 2328. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∀𝑥𝜑 ∧ ∀𝑦𝜓) ↔ ∀𝑥∀𝑦(𝜑 ∧ 𝜓))
Theorem	pm11.57 43148*	Theorem *11.57 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥𝜑 ↔ ∀𝑥∀𝑦(𝜑 ∧ [𝑦 / 𝑥]𝜑))
Theorem	pm11.58 43149*	Theorem *11.58 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥𝜑 ↔ ∃𝑥∃𝑦(𝜑 ∧ [𝑦 / 𝑥]𝜑))
Theorem	pm11.59 43150*	Theorem *11.59 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.)
⊢ (∀𝑥(𝜑 → 𝜓) → ∀𝑦∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → (𝜓 ∧ [𝑦 / 𝑥]𝜓)))
Theorem	pm11.6 43151*	Theorem *11.6 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.)
⊢ (∃𝑥(∃𝑦(𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ∃𝑦(∃𝑥(𝜑 ∧ 𝜒) ∧ 𝜓))
Theorem	pm11.61 43152*	Theorem *11.61 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑦∀𝑥(𝜑 → 𝜓) → ∀𝑥(𝜑 → ∃𝑦𝜓))
Theorem	pm11.62 43153*	Theorem *11.62 in [WhiteheadRussell] p. 166. Importation combined with the rearrangement with quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝜒) ↔ ∀𝑥(𝜑 → ∀𝑦(𝜓 → 𝜒)))
Theorem	pm11.63 43154	Theorem *11.63 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (¬ ∃𝑥∃𝑦𝜑 → ∀𝑥∀𝑦(𝜑 → 𝜓))
Theorem	pm11.7 43155	Theorem *11.7 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥∃𝑦(𝜑 ∨ 𝜑) ↔ ∃𝑥∃𝑦𝜑)
Theorem	pm11.71 43156*	Theorem *11.71 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∃𝑥𝜑 ∧ ∃𝑦𝜒) → ((∀𝑥(𝜑 → 𝜓) ∧ ∀𝑦(𝜒 → 𝜃)) ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))))
21.38.3  Predicate Calculus
Theorem	sbeqal1 43157*	If 𝑥 = 𝑦 always implies 𝑥 = 𝑧, then 𝑦 = 𝑧. (Contributed by Andrew Salmon, 2-Jun-2011.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑧) → 𝑦 = 𝑧)
Theorem	sbeqal1i 43158*	Suppose you know 𝑥 = 𝑦 implies 𝑥 = 𝑧, assuming 𝑥 and 𝑧 are distinct. Then, 𝑦 = 𝑧. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑧)    ⇒   ⊢ 𝑦 = 𝑧
Theorem	sbeqal2i 43159*	If 𝑥 = 𝑦 implies 𝑥 = 𝑧, then we can infer 𝑧 = 𝑦. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑧)    ⇒   ⊢ 𝑧 = 𝑦
Theorem	axc5c4c711 43160	Proof of a theorem that can act as a sole axiom for pure predicate calculus with ax-gen 1798 as the inference rule. This proof extends the idea of axc5c711 37788 and related theorems. (Contributed by Andrew Salmon, 14-Jul-2011.)
⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦(∀𝑦𝜑 → 𝜓) → (𝜑 → ∀𝑦(∀𝑦𝜑 → 𝜓))) → (∀𝑦𝜑 → ∀𝑦𝜓))
Theorem	axc5c4c711toc5 43161	Rederivation of sp 2177 from axc5c4c711 43160. Note that ax6 2384 is used for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) Revised to use ax6v 1973 instead of ax6 2384, so that this rederivation requires only ax6v 1973 and propositional calculus. (Revised by BJ, 14-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	axc5c4c711toc4 43162	Rederivation of axc4 2315 from axc5c4c711 43160. Note that only propositional calculus is required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	axc5c4c711toc7 43163	Rederivation of axc7 2311 from axc5c4c711 43160. Note that neither axc7 2311 nor ax-11 2155 are required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Theorem	axc5c4c711to11 43164	Rederivation of ax-11 2155 from axc5c4c711 43160. Note that ax-11 2155 is not required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	axc11next 43165*	This theorem shows that, given axextb 2707, we can derive a version of axc11n 2426. However, it is weaker than axc11n 2426 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 16-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥)
21.38.4  Principia Mathematica * 13 and * 14
Theorem	pm13.13a 43166	One result of theorem *13.13 in [WhiteheadRussell] p. 178. A note on the section - to make the theorems more usable, and because inequality is notation for set theory (it is not defined in the predicate calculus section), this section will use classes instead of sets. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → [𝐴 / 𝑥]𝜑)
Theorem	pm13.13b 43167	Theorem *13.13 in [WhiteheadRussell] p. 178 with different variable substitution. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ (([𝐴 / 𝑥]𝜑 ∧ 𝑥 = 𝐴) → 𝜑)
Theorem	pm13.14 43168	Theorem *13.14 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ (([𝐴 / 𝑥]𝜑 ∧ ¬ 𝜑) → 𝑥 ≠ 𝐴)
Theorem	pm13.192 43169*	Theorem *13.192 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.)
⊢ (∃𝑦(∀𝑥(𝑥 = 𝐴 ↔ 𝑥 = 𝑦) ∧ 𝜑) ↔ [𝐴 / 𝑦]𝜑)
Theorem	pm13.193 43170	Theorem *13.193 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) ↔ ([𝑦 / 𝑥]𝜑 ∧ 𝑥 = 𝑦))
Theorem	pm13.194 43171	Theorem *13.194 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) ↔ ([𝑦 / 𝑥]𝜑 ∧ 𝜑 ∧ 𝑥 = 𝑦))
Theorem	pm13.195 43172*	Theorem *13.195 in [WhiteheadRussell] p. 179. This theorem is very similar to sbc5 3806. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.)
⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ [𝐴 / 𝑦]𝜑)
Theorem	pm13.196a 43173*	Theorem *13.196 in [WhiteheadRussell] p. 179. The only difference is the position of the substituted variable. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ (¬ 𝜑 ↔ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑦 ≠ 𝑥))
Theorem	2sbc6g 43174*	Theorem *13.21 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑧∀𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) → 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑))
Theorem	2sbc5g 43175*	Theorem *13.22 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∃𝑧∃𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑))
Theorem	iotain 43176	Equivalence between two different forms of ℩. (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ (∃!𝑥𝜑 → ∩ {𝑥 ∣ 𝜑} = (℩𝑥𝜑))
Theorem	iotaexeu 43177	The iota class exists. This theorem does not require ax-nul 5307 for its proof. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
Theorem	iotasbc 43178*	Definition *14.01 in [WhiteheadRussell] p. 184. In Principia Mathematica, Russell and Whitehead define ℩ in terms of a function of (℩𝑥𝜑). Their definition differs in that a function of (℩𝑥𝜑) evaluates to "false" when there isn't a single 𝑥 that satisfies 𝜑. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑦]𝜓 ↔ ∃𝑦(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ 𝜓)))
Theorem	iotasbc2 43179*	Theorem *14.111 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ ((∃!𝑥𝜑 ∧ ∃!𝑥𝜓) → ([(℩𝑥𝜑) / 𝑦][(℩𝑥𝜓) / 𝑧]𝜒 ↔ ∃𝑦∃𝑧(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∀𝑥(𝜓 ↔ 𝑥 = 𝑧) ∧ 𝜒)))
Theorem	pm14.12 43180*	Theorem *14.12 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
Theorem	pm14.122a 43181*	Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝑥 = 𝐴) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ [𝐴 / 𝑥]𝜑)))
Theorem	pm14.122b 43182*	Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → ((∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ [𝐴 / 𝑥]𝜑) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ ∃𝑥𝜑)))
Theorem	pm14.122c 43183*	Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝑥 = 𝐴) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ ∃𝑥𝜑)))
Theorem	pm14.123a 43184*	Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑧∀𝑤(𝜑 ↔ (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑)))
Theorem	pm14.123b 43185*	Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ ∃𝑧∃𝑤𝜑)))
Theorem	pm14.123c 43186*	Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑧∀𝑤(𝜑 ↔ (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ ∃𝑧∃𝑤𝜑)))
Theorem	pm14.18 43187	Theorem *14.18 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → (∀𝑥𝜓 → [(℩𝑥𝜑) / 𝑥]𝜓))
Theorem	iotaequ 43188*	Theorem *14.2 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (℩𝑥𝑥 = 𝑦) = 𝑦
Theorem	iotavalb 43189*	Theorem *14.202 in [WhiteheadRussell] p. 189. A biconditional version of iotaval 6515. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (℩𝑥𝜑) = 𝑦))
Theorem	iotasbc5 43190*	Theorem *14.205 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑦]𝜓 ↔ ∃𝑦(𝑦 = (℩𝑥𝜑) ∧ 𝜓)))
Theorem	pm14.24 43191*	Theorem *14.24 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥𝜑 → ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = (℩𝑥𝜑)))
Theorem	iotavalsb 43192*	Theorem *14.242 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ([𝑦 / 𝑧]𝜓 ↔ [(℩𝑥𝜑) / 𝑧]𝜓))
Theorem	sbiota1 43193	Theorem *14.25 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓))
Theorem	sbaniota 43194	Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓))
Theorem	eubiOLD 43195	Obsolete proof of eubi 2579 as of 7-Oct-2022. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓))
Theorem	iotasbcq 43196	Theorem *14.272 in [WhiteheadRussell] p. 193. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([(℩𝑥𝜑) / 𝑦]𝜒 ↔ [(℩𝑥𝜓) / 𝑦]𝜒))
21.38.5  Set Theory
Theorem	elnev 43197*	Any set that contains one element less than the universe is not equal to it. (Contributed by Andrew Salmon, 16-Jun-2011.)
⊢ (𝐴 ∈ V ↔ {𝑥 ∣ ¬ 𝑥 = 𝐴} ≠ V)
Theorem	rusbcALT 43198	A version of Russell's paradox which is proven using proper substitution. (Contributed by Andrew Salmon, 18-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} ∉ V
Theorem	compeq 43199*	Equality between two ways of saying "the complement of 𝐴". (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ (V ∖ 𝐴) = {𝑥 ∣ ¬ 𝑥 ∈ 𝐴}
Theorem	compne 43200	The complement of 𝐴 is not equal to 𝐴. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 11-Nov-2021.)
⊢ (V ∖ 𝐴) ≠ 𝐴