bj-2uplex - Mathbox for BJ

	Mathbox for BJ		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-2uplex		Structured version Visualization version GIF version

Theorem bj-2uplex 33341

Description: A couple is a set if and only if its coordinates are sets. (Contributed by BJ, 6-Oct-2018.)

**Assertion**
Ref	Expression
bj-2uplex	⊢ (⦅𝐴, 𝐵⦆ ∈ V ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V))

**Proof of Theorem bj-2uplex**
Step	Hyp	Ref	Expression
1		bj-pr21val 33332	. . . 4 ⊢ pr₁ ⦅𝐴, 𝐵⦆ = 𝐴
2		bj-pr1ex 33325	. . . 4 ⊢ (⦅𝐴, 𝐵⦆ ∈ V → pr₁ ⦅𝐴, 𝐵⦆ ∈ V)
3	1, 2	syl5eqelr 2855	. . 3 ⊢ (⦅𝐴, 𝐵⦆ ∈ V → 𝐴 ∈ V)
4		bj-pr22val 33338	. . . 4 ⊢ pr₂ ⦅𝐴, 𝐵⦆ = 𝐵
5		bj-pr2ex 33339	. . . 4 ⊢ (⦅𝐴, 𝐵⦆ ∈ V → pr₂ ⦅𝐴, 𝐵⦆ ∈ V)
6	4, 5	syl5eqelr 2855	. . 3 ⊢ (⦅𝐴, 𝐵⦆ ∈ V → 𝐵 ∈ V)
7	3, 6	jca 501	. 2 ⊢ (⦅𝐴, 𝐵⦆ ∈ V → (𝐴 ∈ V ∧ 𝐵 ∈ V))
8		df-bj-2upl 33330	. . 3 ⊢ ⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1_𝑜} × tag 𝐵))
9		bj-1uplex 33327	. . . . 5 ⊢ (⦅𝐴⦆ ∈ V ↔ 𝐴 ∈ V)
10	9	biimpri 218	. . . 4 ⊢ (𝐴 ∈ V → ⦅𝐴⦆ ∈ V)
11		snex 5036	. . . . 5 ⊢ {1_𝑜} ∈ V
12		bj-xtagex 33308	. . . . 5 ⊢ ({1_𝑜} ∈ V → (𝐵 ∈ V → ({1_𝑜} × tag 𝐵) ∈ V))
13	11, 12	ax-mp 5	. . . 4 ⊢ (𝐵 ∈ V → ({1_𝑜} × tag 𝐵) ∈ V)
14		unexg 7106	. . . 4 ⊢ ((⦅𝐴⦆ ∈ V ∧ ({1_𝑜} × tag 𝐵) ∈ V) → (⦅𝐴⦆ ∪ ({1_𝑜} × tag 𝐵)) ∈ V)
15	10, 13, 14	syl2an 583	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (⦅𝐴⦆ ∪ ({1_𝑜} × tag 𝐵)) ∈ V)
16	8, 15	syl5eqel 2854	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ⦅𝐴, 𝐵⦆ ∈ V)
17	7, 16	impbii 199	1 ⊢ (⦅𝐴, 𝐵⦆ ∈ V ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 ∈ wcel 2145 Vcvv 3351 ∪ cun 3721 {csn 4316 × cxp 5247 1_𝑜c1o 7706 tag bj-ctag 33293 ⦅bj-c1upl 33316 pr₁ bj-cpr1 33319 ⦅bj-c2uple 33329 pr₂ bj-cpr2 33333

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-rep 4904 ax-sep 4915 ax-nul 4923 ax-pow 4974 ax-pr 5034 ax-un 7096

This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3or 1072 df-3an 1073 df-tru 1634 df-fal 1637 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-sbc 3588 df-csb 3683 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-pss 3739 df-nul 4064 df-if 4226 df-pw 4299 df-sn 4317 df-pr 4319 df-tp 4321 df-op 4323 df-uni 4575 df-br 4787 df-opab 4847 df-tr 4887 df-eprel 5162 df-po 5170 df-so 5171 df-fr 5208 df-we 5210 df-xp 5255 df-rel 5256 df-cnv 5257 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 df-ord 5869 df-on 5870 df-suc 5872 df-1o 7713 df-bj-sngl 33285 df-bj-tag 33294 df-bj-proj 33310 df-bj-1upl 33317 df-bj-pr1 33320 df-bj-2upl 33330 df-bj-pr2 33334

This theorem is referenced by: (None)

W3C validator