Theorem abrexexg 7525

Description: Existence of a class abstraction of existentially restricted sets. The class 𝐵 can be thought of as an expression in 𝑥 (which is typically a free variable in the class expression substituted for 𝐵) and the class abstraction appearing in the statement as the class of values 𝐵 as 𝑥 varies through 𝐴. If the "domain" 𝐴 is a set, then the abstraction is also a set. Therefore, this statement is a kind of Replacement. This can be seen by tracing back through the path mptexg 6857, funex 6855, fnex 6853, resfunexg 6851, and funimaexg 6317. See also abrexex2g 7528. There are partial converses under additional conditions, see for instance abnexg 7342. (Contributed by NM, 3-Nov-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)

Assertion

Ref	Expression
abrexexg	⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)

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

Allowed substitution hints:   𝐵(𝑥)   𝑉(𝑥,𝑦)

Proof of Theorem abrexexg

Step	Hyp	Ref	Expression
1		eqid 2797	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	rnmpt 5716	. 2 ⊢ ran (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}
3		mptexg 6857	. . 3 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
4		rnexg 7477	. . 3 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V → ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
5	3, 4	syl 17	. 2 ⊢ (𝐴 ∈ 𝑉 → ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
6	2, 5	syl5eqelr 2890	1 ⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)

Syntax hints:   → wi 4   = wceq 1525   ∈ wcel 2083  {cab 2777  ∃wrex 3108  Vcvv 3440   ↦ cmpt 5047  ran crn 5451

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pr 5228  ax-un 7326

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-id 5355  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240

This theorem is referenced by:  abrexex  7526  iunexg  7527  qsexg  8212  wdomd  8898  cardiun  9264  rankcf  10052  sigaclci  31004  satf0suclem  32232  hbtlem1  39229  hbtlem7  39231