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 33010

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 33001	. . . 4 ⊢ pr₁ ⦅𝐴, 𝐵⦆ = 𝐴
2		bj-pr1ex 32994	. . . 4 ⊢ (⦅𝐴, 𝐵⦆ ∈ V → pr₁ ⦅𝐴, 𝐵⦆ ∈ V)
3	1, 2	syl5eqelr 2706	. . 3 ⊢ (⦅𝐴, 𝐵⦆ ∈ V → 𝐴 ∈ V)
4		bj-pr22val 33007	. . . 4 ⊢ pr₂ ⦅𝐴, 𝐵⦆ = 𝐵
5		bj-pr2ex 33008	. . . 4 ⊢ (⦅𝐴, 𝐵⦆ ∈ V → pr₂ ⦅𝐴, 𝐵⦆ ∈ V)
6	4, 5	syl5eqelr 2706	. . 3 ⊢ (⦅𝐴, 𝐵⦆ ∈ V → 𝐵 ∈ V)
7	3, 6	jca 554	. 2 ⊢ (⦅𝐴, 𝐵⦆ ∈ V → (𝐴 ∈ V ∧ 𝐵 ∈ V))
8		df-bj-2upl 32999	. . 3 ⊢ ⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1_𝑜} × tag 𝐵))
9		bj-1uplex 32996	. . . . 5 ⊢ (⦅𝐴⦆ ∈ V ↔ 𝐴 ∈ V)
10	9	biimpri 218	. . . 4 ⊢ (𝐴 ∈ V → ⦅𝐴⦆ ∈ V)
11		snex 4908	. . . . 5 ⊢ {1_𝑜} ∈ V
12		bj-xtagex 32977	. . . . 5 ⊢ ({1_𝑜} ∈ V → (𝐵 ∈ V → ({1_𝑜} × tag 𝐵) ∈ V))
13	11, 12	ax-mp 5	. . . 4 ⊢ (𝐵 ∈ V → ({1_𝑜} × tag 𝐵) ∈ V)
14		unexg 6959	. . . 4 ⊢ ((⦅𝐴⦆ ∈ V ∧ ({1_𝑜} × tag 𝐵) ∈ V) → (⦅𝐴⦆ ∪ ({1_𝑜} × tag 𝐵)) ∈ V)
15	10, 13, 14	syl2an 494	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (⦅𝐴⦆ ∪ ({1_𝑜} × tag 𝐵)) ∈ V)
16	8, 15	syl5eqel 2705	. 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 384 ∈ wcel 1990 Vcvv 3200 ∪ cun 3572 {csn 4177 × cxp 5112 1_𝑜c1o 7553 tag bj-ctag 32962 ⦅bj-c1upl 32985 pr₁ bj-cpr1 32988 ⦅bj-c2uple 32998 pr₂ bj-cpr2 33002

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-xp 5120 df-rel 5121 df-cnv 5122 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-suc 5729 df-1o 7560 df-bj-sngl 32954 df-bj-tag 32963 df-bj-proj 32979 df-bj-1upl 32986 df-bj-pr1 32989 df-bj-2upl 32999 df-bj-pr2 33003

This theorem is referenced by: (None)

W3C validator