Theorem rexpr 2481

Description: Convert an existential quantification over a pair to a disjunction.

Hypotheses

Ref	Expression
ralpr.1	⊢ A ∈ V
ralpr.2	⊢ B ∈ V

Assertion

Ref	Expression
rexpr	⊢ (∃x ∈ {A, B}φ ↔ ([A / x]φ ⋁ [B / x]φ))

Distinct variable groups:   x,A   x,B

Proof of Theorem rexpr

Step	Hyp	Ref	Expression
1		ralpr.1	. . . . 5 ⊢ A ∈ V
2		ralpr.2	. . . . 5 ⊢ B ∈ V
3	1, 2	ralpr 2480	. . . 4 ⊢ (∀x ∈ {A, B} ¬ φ ↔ ([A / x] ¬ φ ⋀ [B / x] ¬ φ))
4		sbcng 2019	. . . . . 6 ⊢ (A ∈ V → ([A / x] ¬ φ ↔ ¬ [A / x]φ))
5	1, 4	ax-mp 7	. . . . 5 ⊢ ([A / x] ¬ φ ↔ ¬ [A / x]φ)
6		sbcng 2019	. . . . . 6 ⊢ (B ∈ V → ([B / x] ¬ φ ↔ ¬ [B / x]φ))
7	2, 6	ax-mp 7	. . . . 5 ⊢ ([B / x] ¬ φ ↔ ¬ [B / x]φ)
8	5, 7	anbi12i 493	. . . 4 ⊢ (([A / x] ¬ φ ⋀ [B / x] ¬ φ) ↔ (¬ [A / x]φ ⋀ ¬ [B / x]φ))
9	3, 8	bitri 180	. . 3 ⊢ (∀x ∈ {A, B} ¬ φ ↔ (¬ [A / x]φ ⋀ ¬ [B / x]φ))
10	9	notbii 194	. 2 ⊢ (¬ ∀x ∈ {A, B} ¬ φ ↔ ¬ (¬ [A / x]φ ⋀ ¬ [B / x]φ))
11		dfrex2 1703	. 2 ⊢ (∃x ∈ {A, B}φ ↔ ¬ ∀x ∈ {A, B} ¬ φ)
12		oran 319	. 2 ⊢ (([A / x]φ ⋁ [B / x]φ) ↔ ¬ (¬ [A / x]φ ⋀ ¬ [B / x]φ))
13	10, 11, 12	3bitr4i 190	1 ⊢ (∃x ∈ {A, B}φ ↔ ([A / x]φ ⋁ [B / x]φ))

Syntax hints:  ¬ wn 2   ↔ wb 153   ⋁ wo 229   ⋀ wa 230   ∈ wcel 999  [wsbc 1212  ∀wral 1692  ∃wrex 1693  Vcvv 1858  {cpr 2462

This theorem is referenced by:  r19.12sn 2496

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518  df-ral 1696  df-rex 1697  df-v 1859  df-sbc 1989  df-un 2101  df-sn 2464  df-pr 2465

Copyright terms: Public domain