P. 302 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30101-30200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bnj956 30101	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝐴 = 𝐵 → ∀𝑥 𝐴 = 𝐵)    ⇒   ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	bnj976 30102*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 ↔ (𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜑′ ↔ [𝐺 / 𝑓]𝜑)    &   ⊢ (𝜓′ ↔ [𝐺 / 𝑓]𝜓)    &   ⊢ (𝜒′ ↔ [𝐺 / 𝑓]𝜒)    &   ⊢ 𝐺 ∈ V    ⇒   ⊢ (𝜒′ ↔ (𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′))
Theorem	bnj982 30103	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜒 → ∀𝑥𝜒)    &   ⊢ (𝜃 → ∀𝑥𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	bnj1019 30104*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (∃𝑝(𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) ↔ (𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃𝑝𝜏))
Theorem	bnj1023 30105	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ∃𝑥(𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ ∃𝑥(𝜑 → 𝜒)
Theorem	bnj1095 30106	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	bnj1096 30107*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏 ∧ 𝜑))    ⇒   ⊢ (𝜓 → ∀𝑥𝜓)
Theorem	bnj1098 30108*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    ⇒   ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))
Theorem	bnj1101 30109	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ∃𝑥(𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜑)    ⇒   ⊢ ∃𝑥(𝜒 → 𝜓)
Theorem	bnj1113 30110*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷)    ⇒   ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐶 𝐸 = ∪ 𝑥 ∈ 𝐷 𝐸)
Theorem	bnj1109 30111	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ∃𝑥((𝐴 ≠ 𝐵 ∧ 𝜑) → 𝜓)    &   ⊢ ((𝐴 = 𝐵 ∧ 𝜑) → 𝜓)    ⇒   ⊢ ∃𝑥(𝜑 → 𝜓)
Theorem	bnj1131 30112	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜑
Theorem	bnj1138 30113	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = (𝐵 ∪ 𝐶)    ⇒   ⊢ (𝑋 ∈ 𝐴 ↔ (𝑋 ∈ 𝐵 ∨ 𝑋 ∈ 𝐶))
Theorem	bnj1142 30114	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	bnj1143 30115*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵
Theorem	bnj1146 30116*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵
Theorem	bnj1149 30117	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V)
Theorem	bnj1185 30118*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ¬ 𝑤𝑅𝑧)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)
Theorem	bnj1196 30119	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
Theorem	bnj1198 30120	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ (𝜓′ ↔ 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥𝜓′)
Theorem	bnj1209 30121*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 → ∃𝑥 ∈ 𝐵 𝜑)    &   ⊢ (𝜃 ↔ (𝜒 ∧ 𝑥 ∈ 𝐵 ∧ 𝜑))    ⇒   ⊢ (𝜒 → ∃𝑥𝜃)
Theorem	bnj1211 30122	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
Theorem	bnj1213 30123	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ (𝜃 → 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜃 → 𝑥 ∈ 𝐵)
Theorem	bnj1212 30124*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑}    &   ⊢ (𝜃 ↔ (𝜒 ∧ 𝑥 ∈ 𝐵 ∧ 𝜏))    ⇒   ⊢ (𝜃 → 𝑥 ∈ 𝐴)
Theorem	bnj1219 30125	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 ↔ (𝜑 ∧ 𝜓 ∧ 𝜁))    &   ⊢ (𝜃 ↔ (𝜒 ∧ 𝜏 ∧ 𝜂))    ⇒   ⊢ (𝜃 → 𝜓)
Theorem	bnj1224 30126	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ¬ (𝜃 ∧ 𝜏 ∧ 𝜂)    ⇒   ⊢ ((𝜃 ∧ 𝜏) → ¬ 𝜂)
Theorem	bnj1230 30127*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑}    ⇒   ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵)
Theorem	bnj1232 30128	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃 ∧ 𝜏))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	bnj1235 30129	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃 ∧ 𝜏))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	bnj1239 30130	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒) → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	bnj1238 30131	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	bnj1241 30132	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ⊆ 𝐵)
Theorem	bnj1247 30133	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃 ∧ 𝜏))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	bnj1254 30134	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃 ∧ 𝜏))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	bnj1262 30135	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ (𝜑 → 𝐶 = 𝐴)    ⇒   ⊢ (𝜑 → 𝐶 ⊆ 𝐵)
Theorem	bnj1266 30136	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 → ∃𝑥(𝜑 ∧ 𝜓))    ⇒   ⊢ (𝜒 → ∃𝑥𝜓)
Theorem	bnj1265 30137*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	bnj1275 30138	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥(𝜓 ∧ 𝜒))    &   ⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (𝜑 → ∃𝑥(𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	bnj1276 30139	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜒 → ∀𝑥𝜒)    &   ⊢ (𝜃 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜃 → ∀𝑥𝜃)
Theorem	bnj1292 30140	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = (𝐵 ∩ 𝐶)    ⇒   ⊢ 𝐴 ⊆ 𝐵
Theorem	bnj1293 30141	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = (𝐵 ∩ 𝐶)    ⇒   ⊢ 𝐴 ⊆ 𝐶
Theorem	bnj1294 30142	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	bnj1299 30143	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	bnj1304 30144	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜓 → ¬ 𝜒)    ⇒   ⊢ ¬ 𝜑
Theorem	bnj1316 30145*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    &   ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵)    ⇒   ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	bnj1317 30146*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = {𝑥 ∣ 𝜑}    ⇒   ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)
Theorem	bnj1322 30147	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
Theorem	bnj1340 30148	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 → ∃𝑥𝜃)    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝜃))    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ (𝜓 → ∃𝑥𝜒)
Theorem	bnj1345 30149	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥(𝜓 ∧ 𝜒))    &   ⊢ (𝜃 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))    &   ⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (𝜑 → ∃𝑥𝜃)
Theorem	bnj1350 30150*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	bnj1351 30151*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
Theorem	bnj1352 30152*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
Theorem	bnj1361 30153*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	bnj1366 30154*	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 30155*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓)    &   ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔)    &   ⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)))    &   ⊢ (𝜒 ↔ (𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴))    &   ⊢ (𝜃 ↔ (𝜒 ∧ 𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))    &   ⊢ (𝜏 ↔ (𝜃 ∧ 𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))    ⇒   ⊢ (𝜓 → Fun ∪ 𝐴)
Theorem	bnj1383 30156*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓)    &   ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔)    &   ⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)))    ⇒   ⊢ (𝜓 → Fun ∪ 𝐴)
Theorem	bnj1385 30157*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓)    &   ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔)    &   ⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)))    &   ⊢ (𝑥 ∈ 𝐴 → ∀𝑓 𝑥 ∈ 𝐴)    &   ⊢ (𝜑′ ↔ ∀ℎ ∈ 𝐴 Fun ℎ)    &   ⊢ 𝐸 = (dom ℎ ∩ dom 𝑔)    &   ⊢ (𝜓′ ↔ (𝜑′ ∧ ∀ℎ ∈ 𝐴 ∀𝑔 ∈ 𝐴 (ℎ ↾ 𝐸) = (𝑔 ↾ 𝐸)))    ⇒   ⊢ (𝜓 → Fun ∪ 𝐴)
Theorem	bnj1386 30158*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓)    &   ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔)    &   ⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)))    &   ⊢ (𝑥 ∈ 𝐴 → ∀𝑓 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜓 → Fun ∪ 𝐴)
Theorem	bnj1397 30159	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	bnj1400 30160*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥
Theorem	bnj1405 30161*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → 𝑋 ∈ ∪ 𝑦 ∈ 𝐴 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝑋 ∈ 𝐵)
Theorem	bnj1422 30162	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → Fun 𝐴)    &   ⊢ (𝜑 → dom 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 Fn 𝐵)
Theorem	bnj1424 30163	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = (𝐵 ∪ 𝐶)    ⇒   ⊢ (𝐷 ∈ 𝐴 → (𝐷 ∈ 𝐵 ∨ 𝐷 ∈ 𝐶))
Theorem	bnj1436 30164	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = {𝑥 ∣ 𝜑}    ⇒   ⊢ (𝑥 ∈ 𝐴 → 𝜑)
Theorem	bnj1441 30165*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝐴 → ∀𝑦 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → ∀𝑦 𝑧 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})
Theorem	bnj1454 30166	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = {𝑥 ∣ 𝜑}    ⇒   ⊢ (𝐵 ∈ V → (𝐵 ∈ 𝐴 ↔ [𝐵 / 𝑥]𝜑))
Theorem	bnj1459 30167*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐴))    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜒)
Theorem	bnj1464 30168*	Conversion of implicit substitution to explicit class substitution. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))
Theorem	bnj1465 30169*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜒 → 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑉) → ∃𝑥𝜑)
Theorem	bnj1468 30170*	Conversion of implicit substitution to explicit class substitution. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))
Theorem	bnj1476 30171	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}    &   ⊢ (𝜓 → 𝐷 = ∅)    ⇒   ⊢ (𝜓 → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	bnj1502 30172	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → 𝐺 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝐺)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴))
Theorem	bnj1503 30173	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → 𝐺 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝐴 ⊆ dom 𝐺)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴))
Theorem	bnj1517 30174	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = {𝑥 ∣ (𝜑 ∧ 𝜓)}    ⇒   ⊢ (𝑥 ∈ 𝐴 → 𝜓)
Theorem	bnj1521 30175	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 → ∃𝑥 ∈ 𝐵 𝜑)    &   ⊢ (𝜃 ↔ (𝜒 ∧ 𝑥 ∈ 𝐵 ∧ 𝜑))    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ (𝜒 → ∃𝑥𝜃)
Theorem	bnj1533 30176	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜃 → ∀𝑧 ∈ 𝐵 ¬ 𝑧 ∈ 𝐷)    &   ⊢ 𝐵 ⊆ 𝐴    &   ⊢ 𝐷 = {𝑧 ∈ 𝐴 ∣ 𝐶 ≠ 𝐸}    ⇒   ⊢ (𝜃 → ∀𝑧 ∈ 𝐵 𝐶 = 𝐸)
Theorem	bnj1534 30177*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ (𝐻‘𝑥)}    &   ⊢ (𝑤 ∈ 𝐹 → ∀𝑥 𝑤 ∈ 𝐹)    ⇒   ⊢ 𝐷 = {𝑧 ∈ 𝐴 ∣ (𝐹‘𝑧) ≠ (𝐻‘𝑧)}
Theorem	bnj1536 30178*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐵) = (𝐺 ↾ 𝐵))
Theorem	bnj1538 30179	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑}    ⇒   ⊢ (𝑥 ∈ 𝐴 → 𝜑)
Theorem	bnj1541 30180	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝐴 ≠ 𝐵))    &   ⊢ ¬ 𝜑    ⇒   ⊢ (𝜓 → 𝐴 = 𝐵)
Theorem	bnj1542 30181*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐴)    &   ⊢ (𝜑 → 𝐹 ≠ 𝐺)    &   ⊢ (𝑤 ∈ 𝐹 → ∀𝑥 𝑤 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) ≠ (𝐺‘𝑥))
21.4.2  Well founded induction and recursion
Theorem	bnj110 30182*	Well-founded induction restricted to a set (𝐴 ∈ V). The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ (𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))    ⇒   ⊢ ((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	bnj157 30183*	Well-founded induction restricted to a set (𝐴 ∈ V). The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝑅 Fr 𝐴    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	bnj66 30184*	Technical lemma for bnj60 30384. 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.)
⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)}    &   ⊢ 𝑌 = ⟨𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    ⇒   ⊢ (𝑔 ∈ 𝐶 → Rel 𝑔)
Theorem	bnj91 30185*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ ([𝑍 / 𝑦]𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
Theorem	bnj92 30186*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ ([𝑍 / 𝑛]𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑍 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj93 30187*	Technical lemma for bnj97 30190. 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.)
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → pred(𝑥, 𝐴, 𝑅) ∈ V)
Theorem	bnj95 30188	Technical lemma for bnj124 30195. 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.)
⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    ⇒   ⊢ 𝐹 ∈ V
Theorem	bnj96 30189*	Technical lemma for bnj150 30200. 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.) (Revised by Mario Carneiro, 6-May-2015.) (New usage is discouraged.)
⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → dom 𝐹 = 1𝑜)
Theorem	bnj97 30190*	Technical lemma for bnj150 30200. 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.)
⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹‘∅) = pred(𝑥, 𝐴, 𝑅))
Theorem	bnj98 30191	Technical lemma for bnj150 30200. 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.)
⊢ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1𝑜 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))
Theorem	bnj106 30192*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ ([𝐹 / 𝑓][1𝑜 / 𝑛]𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1𝑜 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj118 30193*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜑′ ↔ [1𝑜 / 𝑛]𝜑)    ⇒   ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
Theorem	bnj121 30194*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜁 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜁′ ↔ [1𝑜 / 𝑛]𝜁)    &   ⊢ (𝜑′ ↔ [1𝑜 / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [1𝑜 / 𝑛]𝜓)    ⇒   ⊢ (𝜁′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)))
Theorem	bnj124 30195*	Technical lemma for bnj150 30200. 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.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    &   ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′)    &   ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′)    &   ⊢ (𝜁″ ↔ [𝐹 / 𝑓]𝜁′)    &   ⊢ (𝜁′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)))    ⇒   ⊢ (𝜁″ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 Fn 1𝑜 ∧ 𝜑″ ∧ 𝜓″)))
Theorem	bnj125 30196*	Technical lemma for bnj150 30200. 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.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜑′ ↔ [1𝑜 / 𝑛]𝜑)    &   ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′)    &   ⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    ⇒   ⊢ (𝜑″ ↔ (𝐹‘∅) = pred(𝑥, 𝐴, 𝑅))
Theorem	bnj126 30197*	Technical lemma for bnj150 30200. 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.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜓′ ↔ [1𝑜 / 𝑛]𝜓)    &   ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′)    &   ⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    ⇒   ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1𝑜 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj130 30198*	Technical lemma for bnj151 30201. 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.)
⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜑′ ↔ [1𝑜 / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [1𝑜 / 𝑛]𝜓)    &   ⊢ (𝜃′ ↔ [1𝑜 / 𝑛]𝜃)    ⇒   ⊢ (𝜃′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)))
Theorem	bnj149 30199*	Technical lemma for bnj151 30201. 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.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
⊢ (𝜃1 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃*𝑓(𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)))    &   ⊢ (𝜁0 ↔ (𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜁1 ↔ [𝑔 / 𝑓]𝜁0)    &   ⊢ (𝜑1 ↔ [𝑔 / 𝑓]𝜑′)    &   ⊢ (𝜓1 ↔ [𝑔 / 𝑓]𝜓′)    &   ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    ⇒   ⊢ 𝜃1
Theorem	bnj150 30200*	Technical lemma for bnj151 30201. 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.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜁 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜑′ ↔ [1𝑜 / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [1𝑜 / 𝑛]𝜓)    &   ⊢ (𝜃0 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)))    &   ⊢ (𝜁′ ↔ [1𝑜 / 𝑛]𝜁)    &   ⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    &   ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′)    &   ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′)    &   ⊢ (𝜁″ ↔ [𝐹 / 𝑓]𝜁′)    ⇒   ⊢ 𝜃0