P. 315 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31401-31500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bnj219 31401	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑛 = suc 𝑚 → 𝑚 E 𝑛)
Theorem	bnj226 31402*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶
Theorem	bnj228 31403	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 31404	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	bnj521 31405	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝐴 ∩ {𝐴}) = ∅
Theorem	bnj524 31406	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)
Theorem	bnj525 31407*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜑)
Theorem	bnj534 31408*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 → (∃𝑥𝜑 ∧ 𝜓))    ⇒   ⊢ (𝜒 → ∃𝑥(𝜑 ∧ 𝜓))
Theorem	bnj538 31409*	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 31410	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    ⇒   ⊢ (𝑀 ∈ 𝐷 → ∅ ∈ 𝑀)
Theorem	bnj551 31411	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝑚 = suc 𝑝 ∧ 𝑚 = suc 𝑖) → 𝑝 = 𝑖)
Theorem	bnj563 31412	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 31413	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    ⇒   ⊢ (𝜏 → dom 𝑓 = 𝑚)
Theorem	bnj593 31414	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → ∃𝑥𝜒)
Theorem	bnj596 31415	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥(𝜑 ∧ 𝜓))
Theorem	bnj610 31416*	Pass from equality (𝑥 = 𝐴) to substitution ([𝐴 / 𝑥]) without the distinct variable restriction ($d 𝐴 𝑥). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓′))    &   ⊢ (𝑦 = 𝐴 → (𝜓′ ↔ 𝜓))    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)
Theorem	bnj642 31417	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜑)
Theorem	bnj643 31418	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓)
Theorem	bnj645 31419	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃)
Theorem	bnj658 31420	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	bnj667 31421	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	bnj705 31422	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	bnj706 31423	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	bnj707 31424	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	bnj708 31425	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜃 → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	bnj721 31426	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	bnj832 31427	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓))    &   ⊢ (𝜑 → 𝜏)    ⇒   ⊢ (𝜂 → 𝜏)
Theorem	bnj835 31428	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))    &   ⊢ (𝜑 → 𝜏)    ⇒   ⊢ (𝜂 → 𝜏)
Theorem	bnj836 31429	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))    &   ⊢ (𝜓 → 𝜏)    ⇒   ⊢ (𝜂 → 𝜏)
Theorem	bnj837 31430	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))    &   ⊢ (𝜒 → 𝜏)    ⇒   ⊢ (𝜂 → 𝜏)
Theorem	bnj769 31431	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃))    &   ⊢ (𝜑 → 𝜏)    ⇒   ⊢ (𝜂 → 𝜏)
Theorem	bnj770 31432	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃))    &   ⊢ (𝜓 → 𝜏)    ⇒   ⊢ (𝜂 → 𝜏)
Theorem	bnj771 31433	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃))    &   ⊢ (𝜒 → 𝜏)    ⇒   ⊢ (𝜂 → 𝜏)
Theorem	bnj887 31434	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ 𝜑′)    &   ⊢ (𝜓 ↔ 𝜓′)    &   ⊢ (𝜒 ↔ 𝜒′)    &   ⊢ (𝜃 ↔ 𝜃′)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑′ ∧ 𝜓′ ∧ 𝜒′ ∧ 𝜃′))
Theorem	bnj918 31435	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    ⇒   ⊢ 𝐺 ∈ V
Theorem	bnj919 31436*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝐹 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜑′ ↔ [𝑃 / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [𝑃 / 𝑛]𝜓)    &   ⊢ (𝜒′ ↔ [𝑃 / 𝑛]𝜒)    &   ⊢ 𝑃 ∈ V    ⇒   ⊢ (𝜒′ ↔ (𝑃 ∈ 𝐷 ∧ 𝐹 Fn 𝑃 ∧ 𝜑′ ∧ 𝜓′))
Theorem	bnj923 31437	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    ⇒   ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω)
Theorem	bnj927 31438	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ ((𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛) → 𝐺 Fn 𝑝)
Theorem	bnj930 31439	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    ⇒   ⊢ (𝜑 → Fun 𝐹)
Theorem	bnj931 31440	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = (𝐵 ∪ 𝐶)    ⇒   ⊢ 𝐵 ⊆ 𝐴
Theorem	bnj937 31441*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	bnj941 31442	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    ⇒   ⊢ (𝐶 ∈ V → ((𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛) → 𝐺 Fn 𝑝))
Theorem	bnj945 31443	Technical lemma for bnj69 31677. 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 31444	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
Theorem	bnj951 31445	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜏 → 𝜑)    &   ⊢ (𝜏 → 𝜓)    &   ⊢ (𝜏 → 𝜒)    &   ⊢ (𝜏 → 𝜃)    ⇒   ⊢ (𝜏 → (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	bnj956 31446	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝐴 = 𝐵 → ∀𝑥 𝐴 = 𝐵)    ⇒   ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	bnj976 31447*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 ↔ (𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜑′ ↔ [𝐺 / 𝑓]𝜑)    &   ⊢ (𝜓′ ↔ [𝐺 / 𝑓]𝜓)    &   ⊢ (𝜒′ ↔ [𝐺 / 𝑓]𝜒)    &   ⊢ 𝐺 ∈ V    ⇒   ⊢ (𝜒′ ↔ (𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′))
Theorem	bnj982 31448	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜒 → ∀𝑥𝜒)    &   ⊢ (𝜃 → ∀𝑥𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	bnj1019 31449*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (∃𝑝(𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) ↔ (𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃𝑝𝜏))
Theorem	bnj1023 31450	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ∃𝑥(𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ ∃𝑥(𝜑 → 𝜒)
Theorem	bnj1095 31451	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	bnj1096 31452*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏 ∧ 𝜑))    ⇒   ⊢ (𝜓 → ∀𝑥𝜓)
Theorem	bnj1098 31453*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    ⇒   ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))
Theorem	bnj1101 31454	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ∃𝑥(𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜑)    ⇒   ⊢ ∃𝑥(𝜒 → 𝜓)
Theorem	bnj1113 31455*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷)    ⇒   ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐶 𝐸 = ∪ 𝑥 ∈ 𝐷 𝐸)
Theorem	bnj1109 31456	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ∃𝑥((𝐴 ≠ 𝐵 ∧ 𝜑) → 𝜓)    &   ⊢ ((𝐴 = 𝐵 ∧ 𝜑) → 𝜓)    ⇒   ⊢ ∃𝑥(𝜑 → 𝜓)
Theorem	bnj1131 31457	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜑
Theorem	bnj1138 31458	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = (𝐵 ∪ 𝐶)    ⇒   ⊢ (𝑋 ∈ 𝐴 ↔ (𝑋 ∈ 𝐵 ∨ 𝑋 ∈ 𝐶))
Theorem	bnj1142 31459	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	bnj1143 31460*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵
Theorem	bnj1146 31461*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵
Theorem	bnj1149 31462	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V)
Theorem	bnj1185 31463*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ¬ 𝑤𝑅𝑧)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)
Theorem	bnj1196 31464	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
Theorem	bnj1198 31465	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ (𝜓′ ↔ 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥𝜓′)
Theorem	bnj1209 31466*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 → ∃𝑥 ∈ 𝐵 𝜑)    &   ⊢ (𝜃 ↔ (𝜒 ∧ 𝑥 ∈ 𝐵 ∧ 𝜑))    ⇒   ⊢ (𝜒 → ∃𝑥𝜃)
Theorem	bnj1211 31467	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
Theorem	bnj1213 31468	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ (𝜃 → 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜃 → 𝑥 ∈ 𝐵)
Theorem	bnj1212 31469*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑}    &   ⊢ (𝜃 ↔ (𝜒 ∧ 𝑥 ∈ 𝐵 ∧ 𝜏))    ⇒   ⊢ (𝜃 → 𝑥 ∈ 𝐴)
Theorem	bnj1219 31470	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 ↔ (𝜑 ∧ 𝜓 ∧ 𝜁))    &   ⊢ (𝜃 ↔ (𝜒 ∧ 𝜏 ∧ 𝜂))    ⇒   ⊢ (𝜃 → 𝜓)
Theorem	bnj1224 31471	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ¬ (𝜃 ∧ 𝜏 ∧ 𝜂)    ⇒   ⊢ ((𝜃 ∧ 𝜏) → ¬ 𝜂)
Theorem	bnj1230 31472*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑}    ⇒   ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵)
Theorem	bnj1232 31473	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃 ∧ 𝜏))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	bnj1235 31474	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃 ∧ 𝜏))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	bnj1239 31475	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒) → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	bnj1238 31476	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	bnj1241 31477	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ⊆ 𝐵)
Theorem	bnj1247 31478	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃 ∧ 𝜏))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	bnj1254 31479	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃 ∧ 𝜏))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	bnj1262 31480	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ (𝜑 → 𝐶 = 𝐴)    ⇒   ⊢ (𝜑 → 𝐶 ⊆ 𝐵)
Theorem	bnj1266 31481	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 → ∃𝑥(𝜑 ∧ 𝜓))    ⇒   ⊢ (𝜒 → ∃𝑥𝜓)
Theorem	bnj1265 31482*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	bnj1275 31483	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥(𝜓 ∧ 𝜒))    &   ⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (𝜑 → ∃𝑥(𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	bnj1276 31484	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜒 → ∀𝑥𝜒)    &   ⊢ (𝜃 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜃 → ∀𝑥𝜃)
Theorem	bnj1292 31485	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = (𝐵 ∩ 𝐶)    ⇒   ⊢ 𝐴 ⊆ 𝐵
Theorem	bnj1293 31486	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = (𝐵 ∩ 𝐶)    ⇒   ⊢ 𝐴 ⊆ 𝐶
Theorem	bnj1294 31487	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	bnj1299 31488	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	bnj1304 31489	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜓 → ¬ 𝜒)    ⇒   ⊢ ¬ 𝜑
Theorem	bnj1316 31490*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    &   ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵)    ⇒   ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	bnj1317 31491*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = {𝑥 ∣ 𝜑}    ⇒   ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)
Theorem	bnj1322 31492	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
Theorem	bnj1340 31493	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 → ∃𝑥𝜃)    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝜃))    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ (𝜓 → ∃𝑥𝜒)
Theorem	bnj1345 31494	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥(𝜓 ∧ 𝜒))    &   ⊢ (𝜃 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))    &   ⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (𝜑 → ∃𝑥𝜃)
Theorem	bnj1350 31495*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	bnj1351 31496*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
Theorem	bnj1352 31497*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
Theorem	bnj1361 31498*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	bnj1366 31499*	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 ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦𝜑 ∧ 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑}))    ⇒   ⊢ (𝜓 → 𝐵 ∈ V)
Theorem	bnj1379 31500*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓)    &   ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔)    &   ⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)))    &   ⊢ (𝜒 ↔ (𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴))    &   ⊢ (𝜃 ↔ (𝜒 ∧ 𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))    &   ⊢ (𝜏 ↔ (𝜃 ∧ 𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))    ⇒   ⊢ (𝜓 → Fun ∪ 𝐴)