eqelssd - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > eqelssd		Structured version Visualization version GIF version

Theorem eqelssd 4001

Description: Equality deduction from subclass relationship and membership. (Contributed by AV, 21-Aug-2022.)

**Hypotheses**
Ref	Expression
eqelssd.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
eqelssd.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴)

**Assertion**
Ref	Expression
eqelssd	⊢ (𝜑 → 𝐴 = 𝐵)

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵 𝜑,𝑥

**Proof of Theorem eqelssd**
Step	Hyp	Ref	Expression
1		eqelssd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		eqelssd.2	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴)
3	2	ex 412	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
4	3	ssrdv 3986	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
5	1, 4	eqssd 3997	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1534 ∈ wcel 2099 ⊆ wss 3947

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699

This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3473 df-in 3954 df-ss 3964

This theorem is referenced by: wfrlem10OLD 8338 ordtypelem9 9549 ordtypelem10 9550 oismo 9563 prlem934 11056 phimullem 16747 prmreclem5 16888 psssdm2 18572 sylow3lem3 19583 ablfacrp 20022 isdrng2 20637 imadrhmcl 20684 fidomndrng 21260 pjfo 21648 obs2ss 21662 frlmsslsp 21729 mplbas2 21979 restfpw 23082 2ndcsep 23362 ptclsg 23518 trfg 23794 restutopopn 24142 unirnblps 24324 unirnbl 24325 clsocv 25177 rrxbasefi 25337 pjth 25366 opnmbllem 25529 dvidlem 25843 dvaddf 25872 dvmulf 25873 dvcof 25879 dvcj 25881 dvrec 25886 dvcnv 25908 dvcnvre 25951 ftc1cn 25977 ulmdv 26338 pserdv 26365 ppisval2 27036 noseqrdgfn 28178 nbupgruvtxres 29219 ply1degltdimlem 33316 dimkerim 33321 fedgmul 33325 reff 33440 dya2iocuni 33903 cvmsss2 34884 opnmbllem0 37129 ftc1cnnc 37165 lkrlsp 38574 cdleme50rnlem 40017 hdmaprnN 41337 hgmaprnN 41374 qsalrel 41731 kercvrlsm 42507 pwssplit4 42513 hbtlem5 42552 restuni3 44484 disjf1o 44564 unirnmapsn 44587 iunmapsn 44590 icoiccdif 44909 iccdificc 44924 lptioo2 45019 lptioo1 45020 qndenserrn 45687 intsaluni 45717 iundjiun 45848 meadjiunlem 45853 meaiininclem 45874 iunhoiioo 46064

	
		OSZAR »