P. 334 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33301-33400   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-bnj14 33301*	Define the function giving: the class of all elements of 𝐴 that are "smaller" than 𝑋 according to 𝑅. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ pred(𝑋, 𝐴, 𝑅) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋}
Syntax	w-bnj13 33302	Extend wff notation with the following predicate: 𝑅 is set-like on 𝐴. (New usage is discouraged.)
wff 𝑅 Se 𝐴
Definition	df-bnj13 33303*	Define the following predicate: 𝑅 is set-like on 𝐴. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 pred(𝑥, 𝐴, 𝑅) ∈ V)
Syntax	w-bnj15 33304	Extend wff notation with the following predicate: 𝑅 is both well-founded and set-like on 𝐴. (New usage is discouraged.)
wff 𝑅 FrSe 𝐴
Definition	df-bnj15 33305	Define the following predicate: 𝑅 is both well-founded and set-like on 𝐴. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑅 FrSe 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴))
Syntax	c-bnj18 33306	Extend class notation with the function giving: the transitive closure of 𝑋 in 𝐴 by 𝑅. (New usage is discouraged.)
class trCl(𝑋, 𝐴, 𝑅)
Definition	df-bnj18 33307*	Define the function giving: the transitive closure of 𝑋 in 𝐴 by 𝑅. This definition has been designed for facilitating verification that it is eliminable and that the $d restrictions are sound and complete. For a more readable definition see bnj882 33538. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ trCl(𝑋, 𝐴, 𝑅) = ∪ 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))}∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖)
Syntax	w-bnj19 33308	Extend wff notation with the following predicate: 𝐵 is transitive for 𝐴 and 𝑅. (New usage is discouraged.)
wff TrFo(𝐵, 𝐴, 𝑅)
Definition	df-bnj19 33309*	Define the following predicate: 𝐵 is transitive for 𝐴 and 𝑅. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ( TrFo(𝐵, 𝐴, 𝑅) ↔ ∀𝑥 ∈ 𝐵 pred(𝑥, 𝐴, 𝑅) ⊆ 𝐵)
21.4.1  First-order logic and set theory
Theorem	bnj170 33310	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜑))
Theorem	bnj240 33311	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 → 𝜓′)    &   ⊢ (𝜒 → 𝜒′)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓′ ∧ 𝜒′))
Theorem	bnj248 33312	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃))
Theorem	bnj250 33313	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)))
Theorem	bnj251 33314	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
Theorem	bnj252 33315	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)))
Theorem	bnj253 33316	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃))
Theorem	bnj255 33317	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)))
Theorem	bnj256 33318	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)))
Theorem	bnj257 33319	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜓 ∧ 𝜃 ∧ 𝜒))
Theorem	bnj258 33320	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜃) ∧ 𝜒))
Theorem	bnj268 33321	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓 ∧ 𝜃))
Theorem	bnj290 33322	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜒 ∧ 𝜃 ∧ 𝜓))
Theorem	bnj291 33323	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜓))
Theorem	bnj312 33324	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒 ∧ 𝜃))
Theorem	bnj334 33325	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜑 ∧ 𝜓 ∧ 𝜃))
Theorem	bnj345 33326	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜃 ∧ 𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	bnj422 33327	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃 ∧ 𝜑 ∧ 𝜓))
Theorem	bnj432 33328	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜒 ∧ 𝜃) ∧ (𝜑 ∧ 𝜓)))
Theorem	bnj446 33329	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜑))
Theorem	bnj23 33330*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}    ⇒   ⊢ (∀𝑧 ∈ 𝐵 ¬ 𝑧𝑅𝑦 → ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑦 → [𝑤 / 𝑥]𝜑))
Theorem	bnj31 33331	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒)
Theorem	bnj62 33332*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ([𝑧 / 𝑥]𝑥 Fn 𝐴 ↔ 𝑧 Fn 𝐴)
Theorem	bnj89 33333*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝑍 ∈ V    ⇒   ⊢ ([𝑍 / 𝑦]∃!𝑥𝜑 ↔ ∃!𝑥[𝑍 / 𝑦]𝜑)
Theorem	bnj90 33334*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
⊢ 𝑌 ∈ V    ⇒   ⊢ ([𝑌 / 𝑥]𝑧 Fn 𝑥 ↔ 𝑧 Fn 𝑌)
Theorem	bnj101 33335	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ∃𝑥𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ ∃𝑥𝜓
Theorem	bnj105 33336	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 1o ∈ V
Theorem	bnj115 33337	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜂 ↔ ∀𝑛 ∈ 𝐷 (𝜏 → 𝜃))    ⇒   ⊢ (𝜂 ↔ ∀𝑛((𝑛 ∈ 𝐷 ∧ 𝜏) → 𝜃))
Theorem	bnj132 33338*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∃𝑥(𝜓 → 𝜒))    ⇒   ⊢ (𝜑 ↔ (𝜓 → ∃𝑥𝜒))
Theorem	bnj133 33339	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∃𝑥𝜓)    &   ⊢ (𝜒 ↔ 𝜓)    ⇒   ⊢ (𝜑 ↔ ∃𝑥𝜒)
Theorem	bnj156 33340	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜁0 ↔ (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜁1 ↔ [𝑔 / 𝑓]𝜁0)    &   ⊢ (𝜑1 ↔ [𝑔 / 𝑓]𝜑′)    &   ⊢ (𝜓1 ↔ [𝑔 / 𝑓]𝜓′)    ⇒   ⊢ (𝜁1 ↔ (𝑔 Fn 1o ∧ 𝜑1 ∧ 𝜓1))
Theorem	bnj158 33341*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    ⇒   ⊢ (𝑚 ∈ 𝐷 → ∃𝑝 ∈ ω 𝑚 = suc 𝑝)
Theorem	bnj168 33342*	First-order logic and set theory. Revised to remove dependence on ax-reg 9528. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by NM, 21-Dec-2016.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    ⇒   ⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚 ∈ 𝐷 𝑛 = suc 𝑚)
Theorem	bnj206 33343	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑′ ↔ [𝑀 / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [𝑀 / 𝑛]𝜓)    &   ⊢ (𝜒′ ↔ [𝑀 / 𝑛]𝜒)    &   ⊢ 𝑀 ∈ V    ⇒   ⊢ ([𝑀 / 𝑛](𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑′ ∧ 𝜓′ ∧ 𝜒′))
Theorem	bnj216 33344	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 = suc 𝐵 → 𝐵 ∈ 𝐴)
Theorem	bnj219 33345	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑛 = suc 𝑚 → 𝑚 E 𝑛)
Theorem	bnj226 33346*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶
Theorem	bnj228 33347	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
Theorem	bnj519 33348	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by Mario Carneiro, 6-May-2015.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∈ V → Fun {⟨𝐴, 𝐵⟩})
Theorem	bnj524 33349	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)
Theorem	bnj525 33350*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜑)
Theorem	bnj534 33351*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 → (∃𝑥𝜑 ∧ 𝜓))    ⇒   ⊢ (𝜒 → ∃𝑥(𝜑 ∧ 𝜓))
Theorem	bnj538 33352*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) (Proof shortened by OpenAI, 30-Mar-2020.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑦]∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐵 [𝐴 / 𝑦]𝜑)
Theorem	bnj529 33353	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    ⇒   ⊢ (𝑀 ∈ 𝐷 → ∅ ∈ 𝑀)
Theorem	bnj551 33354	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝑚 = suc 𝑝 ∧ 𝑚 = suc 𝑖) → 𝑝 = 𝑖)
Theorem	bnj563 33355	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ (𝜌 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖))    ⇒   ⊢ ((𝜂 ∧ 𝜌) → suc 𝑖 ∈ 𝑚)
Theorem	bnj564 33356	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    ⇒   ⊢ (𝜏 → dom 𝑓 = 𝑚)
Theorem	bnj593 33357	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → ∃𝑥𝜒)
Theorem	bnj596 33358	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥(𝜑 ∧ 𝜓))
Theorem	bnj610 33359*	Pass from equality (𝑥 = 𝐴) to substitution ([𝐴 / 𝑥]) without the distinct variable condition on 𝐴, 𝑥. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓′))    &   ⊢ (𝑦 = 𝐴 → (𝜓′ ↔ 𝜓))    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)
Theorem	bnj642 33360	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜑)
Theorem	bnj643 33361	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓)
Theorem	bnj645 33362	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃)
Theorem	bnj658 33363	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	bnj667 33364	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	bnj705 33365	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	bnj706 33366	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	bnj707 33367	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	bnj708 33368	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜃 → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	bnj721 33369	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	bnj832 33370	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓))    &   ⊢ (𝜑 → 𝜏)    ⇒   ⊢ (𝜂 → 𝜏)
Theorem	bnj835 33371	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))    &   ⊢ (𝜑 → 𝜏)    ⇒   ⊢ (𝜂 → 𝜏)
Theorem	bnj836 33372	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))    &   ⊢ (𝜓 → 𝜏)    ⇒   ⊢ (𝜂 → 𝜏)
Theorem	bnj837 33373	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))    &   ⊢ (𝜒 → 𝜏)    ⇒   ⊢ (𝜂 → 𝜏)
Theorem	bnj769 33374	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃))    &   ⊢ (𝜑 → 𝜏)    ⇒   ⊢ (𝜂 → 𝜏)
Theorem	bnj770 33375	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃))    &   ⊢ (𝜓 → 𝜏)    ⇒   ⊢ (𝜂 → 𝜏)
Theorem	bnj771 33376	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃))    &   ⊢ (𝜒 → 𝜏)    ⇒   ⊢ (𝜂 → 𝜏)
Theorem	bnj887 33377	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ 𝜑′)    &   ⊢ (𝜓 ↔ 𝜓′)    &   ⊢ (𝜒 ↔ 𝜒′)    &   ⊢ (𝜃 ↔ 𝜃′)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑′ ∧ 𝜓′ ∧ 𝜒′ ∧ 𝜃′))
Theorem	bnj918 33378	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    ⇒   ⊢ 𝐺 ∈ V
Theorem	bnj919 33379*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝐹 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜑′ ↔ [𝑃 / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [𝑃 / 𝑛]𝜓)    &   ⊢ (𝜒′ ↔ [𝑃 / 𝑛]𝜒)    &   ⊢ 𝑃 ∈ V    ⇒   ⊢ (𝜒′ ↔ (𝑃 ∈ 𝐷 ∧ 𝐹 Fn 𝑃 ∧ 𝜑′ ∧ 𝜓′))
Theorem	bnj923 33380	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    ⇒   ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω)
Theorem	bnj927 33381	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ ((𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛) → 𝐺 Fn 𝑝)
Theorem	bnj931 33382	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = (𝐵 ∪ 𝐶)    ⇒   ⊢ 𝐵 ⊆ 𝐴
Theorem	bnj937 33383*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	bnj941 33384	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    ⇒   ⊢ (𝐶 ∈ V → ((𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛) → 𝐺 Fn 𝑝))
Theorem	bnj945 33385	Technical lemma for bnj69 33622. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    ⇒   ⊢ ((𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝐴 ∈ 𝑛) → (𝐺‘𝐴) = (𝑓‘𝐴))
Theorem	bnj946 33386	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
Theorem	bnj951 33387	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜏 → 𝜑)    &   ⊢ (𝜏 → 𝜓)    &   ⊢ (𝜏 → 𝜒)    &   ⊢ (𝜏 → 𝜃)    ⇒   ⊢ (𝜏 → (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	bnj956 33388	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝐴 = 𝐵 → ∀𝑥 𝐴 = 𝐵)    ⇒   ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	bnj976 33389*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 ↔ (𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜑′ ↔ [𝐺 / 𝑓]𝜑)    &   ⊢ (𝜓′ ↔ [𝐺 / 𝑓]𝜓)    &   ⊢ (𝜒′ ↔ [𝐺 / 𝑓]𝜒)    &   ⊢ 𝐺 ∈ V    ⇒   ⊢ (𝜒′ ↔ (𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′))
Theorem	bnj982 33390	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜒 → ∀𝑥𝜒)    &   ⊢ (𝜃 → ∀𝑥𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	bnj1019 33391*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (∃𝑝(𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) ↔ (𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃𝑝𝜏))
Theorem	bnj1023 33392	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ∃𝑥(𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ ∃𝑥(𝜑 → 𝜒)
Theorem	bnj1095 33393	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	bnj1096 33394*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏 ∧ 𝜑))    ⇒   ⊢ (𝜓 → ∀𝑥𝜓)
Theorem	bnj1098 33395*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    ⇒   ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))
Theorem	bnj1101 33396	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ∃𝑥(𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜑)    ⇒   ⊢ ∃𝑥(𝜒 → 𝜓)
Theorem	bnj1113 33397*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷)    ⇒   ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐶 𝐸 = ∪ 𝑥 ∈ 𝐷 𝐸)
Theorem	bnj1109 33398	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ∃𝑥((𝐴 ≠ 𝐵 ∧ 𝜑) → 𝜓)    &   ⊢ ((𝐴 = 𝐵 ∧ 𝜑) → 𝜓)    ⇒   ⊢ ∃𝑥(𝜑 → 𝜓)
Theorem	bnj1131 33399	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜑
Theorem	bnj1138 33400	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = (𝐵 ∪ 𝐶)    ⇒   ⊢ (𝑋 ∈ 𝐴 ↔ (𝑋 ∈ 𝐵 ∨ 𝑋 ∈ 𝐶))