Theorem onfrALTlem1VD 45598

Description: Virtual deduction proof of onfrALTlem1 45257. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALTlem1 45257 is onfrALTlem1VD 45598 without virtual deductions and was automatically derived from onfrALTlem1VD 45598.

1::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   )
2:1:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑥(𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   )
3:2:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦[𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)    )
4::	⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅ ) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
5:4:	⊢ ∀𝑦([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
6:5:	⊢ (∃𝑦[𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
7:3,6:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)   )
8::	⊢ (∃𝑦 ∈ 𝑎(𝑎 ∩ 𝑦) = ∅ ↔ ∃𝑦( 𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
qed:7,8:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ 𝑎(𝑎 ∩ 𝑦) = ∅   )

(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
onfrALTlem1VD	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅   )

Distinct variable group:   𝑥,𝑎,𝑦

Proof of Theorem onfrALTlem1VD

Step	Hyp	Ref	Expression
1		idn2 45322	. . . . 5 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   )
2		19.8a 2217	. . . . 5 ⊢ ((𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) → ∃𝑥(𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅))
3	1, 2	e2 45340	. . . 4 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑥(𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   )
4		cbvexsv 45256	. . . . 5 ⊢ (∃𝑥(𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ ∃𝑦[𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅))
5	4	biimpi 219	. . . 4 ⊢ (∃𝑥(𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) → ∃𝑦[𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅))
6	3, 5	e2 45340	. . 3 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦[𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   )
7		sbsbc 3748	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅))
8		onfrALTlem4 45252	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
9	7, 8	bitri 278	. . . . 5 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
10	9	ax-gen 1825	. . . 4 ⊢ ∀𝑦([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
11		exbi 1877	. . . 4 ⊢ (∀𝑦([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)) → (∃𝑦[𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)))
12	10, 11	e0a 45480	. . 3 ⊢ (∃𝑦[𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
13	6, 12	e2bi 45341	. 2 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)   )
14		df-rex 3090	. 2 ⊢ (∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅ ↔ ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
15	13, 14	e2bir 45342	1 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅   )

Syntax hints:   ↔ wb 209   ∧ wa 400  ∀wal 1568   = wceq 1570  ∃wex 1809  [wsb 2096   ∈ wcel 2143   ≠ wne 2958  ∃wrex 3089  [wsbc 3744   ∩ cin 3904   ⊆ wss 3905  ∅c0 4286  Oncon0 6360  (   wvd2 45286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-13 2404  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-in 3912  df-nul 4287  df-vd2 45287

This theorem is referenced by:  onfrALTVD  45599